Michael Soegtrop (Mar 30 2022 at 15:43): 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.
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.
Michael Soegtrop (Mar 30 2022 at 16:18):Yes, I remember now, thanks. I think I fixed it.
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
Karl Palmskog (Mar 31 2022 at 08:26):predict is a C program bundled with coq-hammer
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?
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.
Karl Palmskog (Mar 31 2022 at 11:46):OK, there are actually two binaries provided by coq-hammer: predict and htimeout
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.
Michael Soegtrop (Mar 31 2022 at 12:30):Eventually I should merge this with the mechanism used for the Windows installer.
Last updated: Jun 03 2023 at 04:30 UTC