Stream: Hierarchy Builder devs & users

Topic: compilation with hierarchy-builder

Reynald Affeldt (Sep 11 2020 at 13:34):

We have this PR on mathcomp-analysis that uses hierarchy-builder : https://github.com/math-comp/analysis/pull/253 .
It compiles fine on my laptop with hierarchy-builder.0.10.0 and Coq 8.12 (all via opam) but the CI fails.
I can't guess what is wrong by looking at the build output.
Would you have a hint?

Enrico Tassi (Sep 11 2020 at 13:53):

O_o

Enrico Tassi (Sep 11 2020 at 13:53):

wow

Enrico Tassi (Sep 11 2020 at 13:53):

I know nothing about nix, but I see

unpacking 'https://github.com/math-comp/math-comp-nix/archive/master.tar.gz'...
unpacking 'https://github.com/CohenCyril/nixpkgs/archive/mathcomp-1.11fix.tar.gz'...
unpacking 'https://github.com/math-comp/math-comp/archive/mathcomp-1.11.0.tar.gz'...
unpacking 'https://github.com/math-comp/finmap/archive/master.tar.gz'...
unpacking 'https://github.com/math-comp/bigenough/archive/master.tar.gz'...
unpacking 'https://github.com/math-comp/real-closed/archive/master.tar.gz'...
unpacking 'https://github.com/math-comp/analysis/archive/integral_sketch_hb.tar.gz'...

and nothing about HB... is there a nix file to update?

Reynald Affeldt (Sep 11 2020 at 13:57):

There is confix.nix with this contents:

{
  coq = "8.10";
  mathcomp = "mathcomp-1.11.0";
  mathcomp-real-closed = "1.1.1";
}

Reynald Affeldt (Sep 11 2020 at 13:58):

It might be that I need to add some entry for hb but the format does not look uniform :-)

Enrico Tassi (Sep 11 2020 at 13:58):

These looks like tag names

Enrico Tassi (Sep 11 2020 at 13:59):

or at least, the git tags in MC are named mathcomp-$version (probably my fault)

Enrico Tassi (Sep 11 2020 at 14:00):

A ghost from the cvs/svn era... since I'm not a big fan of v$version I did choose mathcomp- in place of v, but in git a tag can just be a number :-/

Reynald Affeldt (Sep 11 2020 at 14:01):

so it might be "v0.10.0" because of https://github.com/math-comp/hierarchy-builder/releases/tag/v0.10.0 ?

Enrico Tassi (Sep 11 2020 at 14:01):

Hem... I guess so

Reynald Affeldt (Sep 11 2020 at 14:01):

Enrico Tassi said:

A ghost from the cvs/svn era... since I'm not a big fan of v$version I did choose mathcomp- in place of v, but in git a tag can just be a number :-/

Wait... The tag for hb starts with a "v" ^_^

Enrico Tassi (Sep 11 2020 at 14:03):

I'll go find my sackcloth ;-)

Last updated: Sep 09 2024 at 04:02 UTC