Stream: Hierarchy Builder devs & users

Topic: installation and mathcomp


view this post on Zulip Marie Kerjean (Mar 23 2021 at 09:58):

In the process of learning HB, I cloned the partial port of mathcomp available here, but I get an error. When compiling math-comp, I get the error

File "./ssreflect/eqtype.v", line 131, characters 36-47:
Error: The reference Equality.on was not found in the current environment.

when HB is launched with opam. When using nix, I get the error:

File "./ssreflect/eqtype.v", line 126, characters 0-86:
Error: Attribute mathcomp.axiom is not supported

What did I do wrong ?

view this post on Zulip Enrico Tassi (Mar 23 2021 at 10:17):

Looks like you are using a released version, which is fine, but the port of mathcomp really needs the very last commits.
I can only suggest a fix for opam, this should do it:

opam pin add coq-hierarchy-builder https://github.com/math-comp/hierarchy-builder.git

It will download the very last commit and install it.

BTW we should really make a new release soonish @Cyril Cohen , for sure before the 6th of April

view this post on Zulip Marie Kerjean (Mar 23 2021 at 10:19):

Thanks :-D !

view this post on Zulip Marie Kerjean (Mar 23 2021 at 10:24):

Is there a specific version of Coq or Ocaml I should have to install the dev version ?

view this post on Zulip Enrico Tassi (Mar 23 2021 at 10:27):

Coq 8.13

view this post on Zulip Enrico Tassi (Mar 23 2021 at 10:27):

No, actually it also works with 8.12 and 8.11

view this post on Zulip Enrico Tassi (Mar 23 2021 at 10:31):

CI tests it for us on 8.11, 8.12 and 8.13. So if you have already one installed, just use it. If you are making a new switch then I recommend 8.13 since a few (optional) features will only work on 8.13

view this post on Zulip Cyril Cohen (Mar 23 2021 at 11:45):

Yep; actually we should release now

view this post on Zulip Cyril Cohen (Mar 23 2021 at 11:47):

@Marie Kerjean if you are still using nix, there is a working nix shell available in the mathcomp partial port branch. You just need to type
nix-shell from the root directory of the repo to get coq 8.13, and working versions of elpi, coq-elpi and hierarchy-builder

view this post on Zulip Cyril Cohen (Mar 23 2021 at 11:48):

Or not, it seems to be broken... because I put no CI to test it, I will fix this and put a CI

view this post on Zulip Cyril Cohen (Mar 23 2021 at 11:48):

(CI should really be mandatory...)

view this post on Zulip Cyril Cohen (Mar 23 2021 at 11:49):

I will fix it, now

view this post on Zulip Cyril Cohen (Mar 23 2021 at 12:52):

@Marie Kerjean fixed!

view this post on Zulip Cyril Cohen (Mar 23 2021 at 12:53):

You can now do what I said...

view this post on Zulip Cyril Cohen (Mar 23 2021 at 12:55):

nix-shell inside the current upstream/hierarchy-builder branch should put you in a state where everything is available.

view this post on Zulip Cyril Cohen (Mar 23 2021 at 15:11):

@Marie Kerjean you will tell me if it worked for you?

view this post on Zulip Marie Kerjean (Mar 23 2021 at 18:03):

@Cyril Cohen I just tested it and it works :-) ! Thank you very much !

view this post on Zulip Marie Kerjean (Apr 15 2021 at 08:56):

What should I add to a nix config file if I want to make a repository depend on hierarchy-builder ? I tried to merge the mathcomp/hierarchy builder config file and the analysis one but it's seems too naïve.

view this post on Zulip Cyril Cohen (Apr 15 2021 at 12:11):

Marie Kerjean said:

What should I add to a nix config file if I want to make a repository depend on hierarchy-builder ? I tried to merge the mathcomp/hierarchy builder config file and the analysis one but it's seems too naïve.

It's my fault, I did not upgrade mathcomp/analysis CI to the new toolbox, yet

view this post on Zulip Marie Kerjean (Apr 15 2021 at 12:38):

There's no hurry, I just wanted to test HB on analysis since it's the library I know best, but it's only for learning purposes.

view this post on Zulip Cyril Cohen (Apr 15 2021 at 12:39):

We plan to release the toolbox very soon and as soon as it is released I will update it everywhere...


Last updated: Jan 29 2023 at 15:02 UTC