Marie Kerjean (Mar 23 2021 at 09:58): 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 ?
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
Marie Kerjean (Mar 23 2021 at 10:19):Thanks :-D !
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 ?
Enrico Tassi (Mar 23 2021 at 10:27):Coq 8.13
Enrico Tassi (Mar 23 2021 at 10:27):No, actually it also works with 8.12 and 8.11
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
Cyril Cohen (Mar 23 2021 at 11:45):Yep; actually we should release now
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
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
Cyril Cohen (Mar 23 2021 at 11:48):(CI should really be mandatory...)
Cyril Cohen (Mar 23 2021 at 11:49):I will fix it, now
Cyril Cohen (Mar 23 2021 at 12:52):@Marie Kerjean fixed!
Cyril Cohen (Mar 23 2021 at 12:53):You can now do what I said...
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.
Cyril Cohen (Mar 23 2021 at 15:11):@Marie Kerjean you will tell me if it worked for you?
Marie Kerjean (Mar 23 2021 at 18:03):@Cyril Cohen I just tested it and it works :-) ! Thank you very much !
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.
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
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.
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: May 28 2023 at 18:29 UTC