I just tried AAC Tactics on a fairly recent commit to
master, and it doesn't build:
File "src/coq.ml", line 87, characters 19-52: 87 | let sigma, env = Declare.Proof.get_current_context pstate in ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Unbound value Declare.Proof.get_current_context
Has this been fixed recently, or what's going on? All my recent cron'd Travis jobs have failed also.
(I'm surprised since there haven't been any PRs to merge lately.)
AFAICT this has been changed quite a long time ago in #12372
Some time in June
Isn't AAC Tactics supposed to be in Coq's CI though. Would it mean that it is not properly or only partially tested there?
Right, I was mistaken, the code looks fine actually.
@Karl Palmskog are you sure you have the right Coq version in PATH?
ah, I was indeed using the wrong version in the PATH, here is apparently the problem in the cronjobs (https://travis-ci.com/github/coq-community/aac-tactics/jobs/383240531):
ocamlfind: Package `zarith' not found
we probably need to update the Nix configurations in a lot of places...
@Théo Zimmermann so is it the following in
default.nix that needs to be changed to include zarith?:
buildInputs = with coq.ocamlPackages; [ ocaml findlib ]
It's probably an issue very similar to the one with had with
so you want to fix it upstream instead? Indeed, it looks like the choice is either solving as for num upstream, or every plugin using Nix adds it (but this could be accommodated by our template and
https://github.com/coq/coq/pull/13015 fixes this
Last updated: Dec 05 2023 at 05:01 UTC