Karl Palmskog (Sep 11 2020 at 11:10): Karl Palmskog (Sep 11 2020 at 11:10):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.)
Pierre-Marie Pédrot (Sep 11 2020 at 11:51):AFAICT this has been changed quite a long time ago in #12372
Pierre-Marie Pédrot (Sep 11 2020 at 11:51):Some time in June
Théo Zimmermann (Sep 11 2020 at 11:56):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?
Pierre-Marie Pédrot (Sep 11 2020 at 11:58):Right, I was mistaken, the code looks fine actually.
Pierre-Marie Pédrot (Sep 11 2020 at 11:59):@Karl Palmskog are you sure you have the right Coq version in PATH?
Karl Palmskog (Sep 11 2020 at 12:03):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...
Karl Palmskog (Sep 11 2020 at 12:18):@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 num
Karl Palmskog (Sep 11 2020 at 14:23):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 plugin: true)
Théo Zimmermann (Sep 11 2020 at 14:43):Yes
Théo Zimmermann (Sep 11 2020 at 15:02):https://github.com/coq/coq/pull/13015 fixes this
Last updated: Sep 09 2024 at 05:02 UTC