Stream: Coq Platform devs & users

Topic: ATPs for Coq Hammer in Snap not installed


view this post on Zulip Michael Soegtrop (Mar 30 2022 at 15:43):

@Enrico Tassi : can you please have a look at this CI run: https://github.com/coq/platform/actions/runs/2064098903

The issue here is that the ATPs (Eprover and Z3_tptp) are not installed. I guess it was always like this - I just added two new smoke test cases which test if the ATPs are actually there (the previous smoke test only tested reconstruction of proofs).

Do you have an idea why the ATPs are not installed? They should be in the opam bin and possibly lib folders.

view this post on Zulip Enrico Tassi (Mar 30 2022 at 16:00):

I guess it is the usual line that cleans up too many things from the opam root.

view this post on Zulip Michael Soegtrop (Mar 30 2022 at 16:18):

Yes, I remember now, thanks. I think I fixed it.

view this post on Zulip Michael Soegtrop (Mar 31 2022 at 08:23):

Hmm, it now does find the provers but can't run them ...
https://github.com/coq/platform/runs/5760001738?check_suite_focus=true#step:6:3123

view this post on Zulip Karl Palmskog (Mar 31 2022 at 08:26):

predict is a C program bundled with coq-hammer

view this post on Zulip Karl Palmskog (Mar 31 2022 at 08:29):

since prediction failed, provers were never invoked. Could it have something to do with access rights in CI? Can the process write to /tmp?

view this post on Zulip Michael Soegtrop (Mar 31 2022 at 11:44):

@Karl Palmskog : thanks - and no, the issue is that the snap generator applies a positive list filtering on what it includes, and this need to be extended.

view this post on Zulip Karl Palmskog (Mar 31 2022 at 11:46):

OK, there are actually two binaries provided by coq-hammer: predict and htimeout

view this post on Zulip Michael Soegtrop (Mar 31 2022 at 12:30):

@Karl Palmskog : yes - I changed the positive list to a negative list - this should be more robust.

view this post on Zulip Michael Soegtrop (Mar 31 2022 at 12:30):

Eventually I should merge this with the mechanism used for the Windows installer.


Last updated: Jan 30 2023 at 10:03 UTC