diff --git a/.gitignore b/.gitignore index 7eab233b8..e92c1e871 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ +metacoq-config .history docs/_site *.annot diff --git a/configure.sh b/configure.sh index fdd968c6f..d81dcce81 100755 --- a/configure.sh +++ b/configure.sh @@ -20,7 +20,10 @@ then PCUIC_DEPS="-R ../template-coq/theories MetaCoq.Template" SAFECHECKER_DEPS="-R ../pcuic/theories MetaCoq.PCUIC" ERASURE_DEPS="-R ../safechecker/theories MetaCoq.SafeChecker" - TRANSLATIONS_DEPS="" + TRANSLATIONS_DEPS="-I ../template-coq" + EXAMPLES_DEPS="-R ../erasure/theories MetaCoq.Erasure" + TEST_SUITE_DEPS="-R ../erasure/theories MetaCoq.Erasure" + PLUGIN_DEMO_DEPS="-R ../../template-coq/theories MetaCoq.Template -I ../../template-coq/" echo "METACOQ_CONFIG = local" > Makefile.conf else echo "Building MetaCoq globally (default)" @@ -28,6 +31,9 @@ then SAFECHECKER_DEPS="" ERASURE_DEPS="" TRANSLATIONS_DEPS="" + EXAMPLES_DEPS="" + TEST_SUITE_DEPS="" + PLUGIN_DEMO_DEPS="" echo "METACOQ_CONFIG = global" > Makefile.conf fi @@ -35,11 +41,18 @@ then echo "# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh" > safechecker/metacoq-config echo "# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh" > erasure/metacoq-config echo "# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh" > translations/metacoq-config + echo "# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh" > examples/metacoq-config + echo "# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh" > test-suite/metacoq-config + echo "# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh" > test-suite/plugin-demo/metacoq-config echo ${PCUIC_DEPS} >> pcuic/metacoq-config echo ${PCUIC_DEPS} ${SAFECHECKER_DEPS} >> safechecker/metacoq-config echo ${PCUIC_DEPS} ${SAFECHECKER_DEPS} ${ERASURE_DEPS} >> erasure/metacoq-config echo ${PCUIC_DEPS} ${TRANSLATIONS_DEPS} >> translations/metacoq-config + echo ${PCUIC_DEPS} ${SAFECHECKER_DEPS} ${ERASURE_DEPS} ${TRANSLATIONS_DEPS} ${EXAMPLES_DEPS} >> examples/metacoq-config + echo ${PCUIC_DEPS} ${SAFECHECKER_DEPS} ${ERASURE_DEPS} ${TRANSLATIONS_DEPS} ${TEST_SUITE_DEPS} >> test-suite/metacoq-config + echo ${PLUGIN_DEMO_DEPS} >> test-suite/plugin-demo/metacoq-config + else echo "Error: coqc not found in path" fi diff --git a/translations/_CoqProject.in b/translations/_CoqProject.in index 766846268..a7ba44b02 100644 --- a/translations/_CoqProject.in +++ b/translations/_CoqProject.in @@ -1,5 +1,4 @@ -R . MetaCoq.Translations --I ../template-coq/ sigma.v MiniHoTT.v