Pierre-Marie Pédrot (Oct 14 2022 at 11:21): Pierre-Marie Pédrot (Oct 14 2022 at 11:21):I am happily trying to run the smtcoq CI that just got added locally on my machine but it fails miserably.
Pierre-Marie Pédrot (Oct 14 2022 at 11:22):I am getting
coq_makefile -f _CoqProject -o Makefile
Error: cannot find tools/CoqMakefile.inMakefile:20: Makefile.conf: Aucun fichier ou dossier de ce type
Any idea what's going wrong?
Pierre-Marie Pédrot (Oct 14 2022 at 11:23):I have performed a full make world and I am running make -f Makefile.ci ci-smtcoq
Pierre-Marie Pédrot (Oct 14 2022 at 11:23):(there are a bunch of warnings before as well, indicating that the path is poorly set probably)
Gaëtan Gilbert (Oct 14 2022 at 11:44):broken on my machine too
no idea what's going on
Gaëtan Gilbert (Oct 14 2022 at 11:44):for some reason smtcoq has a checked in generated Makefile with
Makefile.conf: _CoqProject
coq_makefile -f _CoqProject -o Makefile
the real surprise is that it worked in CI
Emilio Jesús Gallego Arias (Oct 14 2022 at 11:46):yeah I wonder how the makefile self destructs
Emilio Jesús Gallego Arias (Oct 14 2022 at 11:46):in CI Coq is installed
Théo Zimmermann (Oct 14 2022 at 13:22):Can we suggest a more classic Makefile structure with no checked in generated Makefile maybe? cc @Chantal Keller
Chantal Keller (Oct 14 2022 at 14:24):Ok, I'll work on that
Chantal Keller (Oct 14 2022 at 16:24):That is done: https://github.com/smtcoq/smtcoq/commit/a726b5d6ad092f177ac096accd3147e1f014bd55
Tell me if you still have problems
Last updated: Apr 19 2024 at 02:02 UTC