Skip to content

Commit

Permalink
Fix configure script w.r.t findlib usage
Browse files Browse the repository at this point in the history
  • Loading branch information
mattam82 committed Sep 21, 2022
1 parent 3a4214b commit 77ae519
Show file tree
Hide file tree
Showing 3 changed files with 15 additions and 2 deletions.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
metacoq-config
.history
docs/_site
*.annot
Expand Down
15 changes: 14 additions & 1 deletion configure.sh
Original file line number Diff line number Diff line change
Expand Up @@ -20,26 +20,39 @@ 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)"
PCUIC_DEPS=""
SAFECHECKER_DEPS=""
ERASURE_DEPS=""
TRANSLATIONS_DEPS=""
EXAMPLES_DEPS=""
TEST_SUITE_DEPS=""
PLUGIN_DEMO_DEPS=""
echo "METACOQ_CONFIG = global" > Makefile.conf
fi

echo "# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh" > pcuic/metacoq-config
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
1 change: 0 additions & 1 deletion translations/_CoqProject.in
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
-R . MetaCoq.Translations
-I ../template-coq/

sigma.v
MiniHoTT.v
Expand Down

0 comments on commit 77ae519

Please sign in to comment.