coqPackages.hierarchy-builder: init at 0.9.0 #82325
Conversation
|
@GrahamcOfBorg build coqPackages_8_10.hierarchy-builder coqPackages_8_11.hierarchy-builder |
| }; | ||
|
|
||
| nativeBuildInputs = [ which ]; | ||
| buildInputs = [ coq coq.ocaml coq.ocamlPackages.elpi coq-elpi ]; |
There was a problem hiding this comment.
coq-elpi should be propagated.
In the current state, running “From HB Require structures.” fails.
There was a problem hiding this comment.
How do you test this quickly?
There was a problem hiding this comment.
I never understand what should be propagated, e.g. shouldn't coq be propagated?
There was a problem hiding this comment.
To test: nix-shell -p coqPackages_8_10.hierarchy-builder coqPackages_8_10.coq and then run coqc on a test case (e.g., https://raw.githubusercontent.com/math-comp/hierarchy-builder/master/demo1/hierarchy_0.v).
Should coq be propagated? No. It is likely to use a different version of Coq to build the package and to use it. In the first case, for instance, we don’t need CoqIDE, the manual etc.
There was a problem hiding this comment.
To test:
nix-shell -p coqPackages_8_10.hierarchy-builder coqPackages_8_10.coq
That's what I tried and it does not work for me:
$ nix-shell -p coqPackages_8_10.hierarchy-builder (hierarchy-builder|✔)
error: attribute 'hierarchy-builder' missing, at (string):1:94
(use '--show-trace' to show detailed location information)
There was a problem hiding this comment.
Let’s start from two identical configurations (same OCaml, same snapshot of the Coq source code). In the first one you run ./configure -coqide no and in the second, you run ./configure -coqide opt.
Are you saying that the fact that using the .vo from the first configuration in the second one does work is a miracle?
I’m still puzzled to get different .cmx files.
There was a problem hiding this comment.
Are you saying that the fact that using the .vo from the first configuration in the second one does work is a miracle?
No, in that case I believe they should be the same looking at today's sources. But even a single #IFDEF COQIDE could break this.
If it does not work today, then I believe there is something very fishy going on.
I'm not familiar with nix. Do you have 1 source - 1 binary as in opam?
There was a problem hiding this comment.
Yeah, it would be nice to have part of the standard library dedicated to CoqIDE users! (just kidding).
Do you have 1 source - 1 binary
What do you mean?
There was a problem hiding this comment.
What I don't know why you would compile coq twice. I debian the output of the compilation of 1 source package can generate many binary packages, so coq & coqide are compiled once and later split. Here you seem to say that you compile the same coq sources twice.
In opam 1 source -> 1 package. So the sources of Coq are used twice, one for compiling coqtop/coqc and one for coqide. Even there, coqc/coqtop (and all its dependencies) are compiled only once (but for a very limited set of files that are linked in both coqtop and coqide)
There was a problem hiding this comment.
@gares in nix, it's 1 derivation -> 1 package, a derivation (roughly) is the data of "the source + the dependencies + the commands that are run to fix the sources, build, fixup stuff and install."
Hence if you tune some compiling options, you might create a different coq binary but you definitely create a new nix coq package.
CohenCyril
force-pushed
the
hierarchy-builder
branch
from
41e38e8
to
684ee31
Compare
CohenCyril
force-pushed
the
hierarchy-builder
branch
from
684ee31
to
d8305d1
Compare
|
@GrahamcOfBorg build coqPackages_8_10.hierarchy-builder coqPackages_8_11.hierarchy-builder |
|
Merged into 20.03 as c07561f |
Motivation for this change
Adding the first release of a new coq package.
Things done
sandboxinnix.confon non-NixOS linux)nix-shell -p nixpkgs-review --run "nixpkgs-review wip"./result/bin/)nix path-info -Sbefore and after)