@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.
I guess it is the usual line that cleans up too many things from the opam root.
Yes, I remember now, thanks. I think I fixed it.
Hmm, it now does find the provers but can't run them ...
predict is a C program bundled with
since prediction failed, provers were never invoked. Could it have something to do with access rights in CI? Can the process write to
@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.
OK, there are actually two binaries provided by
@Karl Palmskog : yes - I changed the positive list to a negative list - this should be more robust.
Eventually I should merge this with the mechanism used for the Windows installer.
Last updated: Jan 30 2023 at 10:03 UTC