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?

O_o

wow

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?

There is `confix.nix`

with this contents:

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

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

These looks like tag names

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

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 :-/

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

Hem... I guess so

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" ^_^

I'll go find my sackcloth ;-)

Last updated: Feb 22 2024 at 03:02 UTC