Stream: Coq devs & plugin devs

Topic: AAC Tactics broken on master?


view this post on Zulip 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.)

view this post on Zulip Pierre-Marie Pédrot (Sep 11 2020 at 11:51):

AFAICT this has been changed quite a long time ago in #12372

view this post on Zulip Pierre-Marie Pédrot (Sep 11 2020 at 11:51):

Some time in June

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Sep 11 2020 at 11:58):

Right, I was mistaken, the code looks fine actually.

view this post on Zulip Pierre-Marie Pédrot (Sep 11 2020 at 11:59):

@Karl Palmskog are you sure you have the right Coq version in PATH?

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Sep 11 2020 at 12:03):

we probably need to update the Nix configurations in a lot of places...

view this post on Zulip 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 ]

view this post on Zulip Théo Zimmermann (Sep 11 2020 at 13:22):

It's probably an issue very similar to the one with had with num

view this post on Zulip 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)

view this post on Zulip Théo Zimmermann (Sep 11 2020 at 14:43):

Yes

view this post on Zulip Théo Zimmermann (Sep 11 2020 at 15:02):

https://github.com/coq/coq/pull/13015 fixes this


Last updated: Oct 16 2021 at 09:07 UTC