Stream: Coq devs & plugin devs

Topic: Local run of the smtcoq CI


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Oct 14 2022 at 11:22):

Any idea what's going wrong?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Gaëtan Gilbert (Oct 14 2022 at 11:44):

broken on my machine too
no idea what's going on

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Oct 14 2022 at 11:45):

the real surprise is that it worked in CI

view this post on Zulip Emilio Jesús Gallego Arias (Oct 14 2022 at 11:46):

yeah I wonder how the makefile self destructs

view this post on Zulip Emilio Jesús Gallego Arias (Oct 14 2022 at 11:46):

in CI Coq is installed

view this post on Zulip 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

view this post on Zulip Chantal Keller (Oct 14 2022 at 14:24):

Ok, I'll work on that

view this post on Zulip 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: Feb 06 2023 at 19:03 UTC