search

coq / coq-bench

Scripts for differential performance testing of Coq packages / versions
Other
4 stars 6 forks source link

bignums failing #83

Closed SkySkimmer closed 4 years ago

SkySkimmer commented 4 years ago 
# (cd _build/default && /home/jenkins/workspace/benchmark-part-of-the-branch/904/opam.NEW/ocaml-base-compiler.4.07.1/bin/coqc -native-compiler yes -I /home/jenkins/workspace/benchmark-part-of-the-branch/904/opam.NEW/ocaml-base-compiler.4.07.1/lib/coq/clib -I /home/jenkins/workspace/benchmark-part-of-the-branch/904/opam.NEW/ocaml-base-compiler.4.07.1/lib/coq/config -I /home/jenkins/workspace/ben[...]
# File "./SpecViaZ/.coq-native/NBignums_SpecViaZ_NSig.native", line 26, characters 2-52:
# Error: Unbound module NCoq_ZArith_BinInt
ejgallego commented 4 years ago

Looks like a bug in coq_makefile ? It should detect that Coq was built with native-compute disabled and don't do this. Even so native is supposed to compile on the fly, maybe the recent changes broke it.

SkySkimmer commented 4 years ago

(cd _build/default means it's dune not coq_makefile no?

ejgallego commented 4 years ago

Where is the -native-compiler yes added? So bizarre.

SkySkimmer commented 4 years ago

https://github.com/coq/bignums/commit/3539b53b0a3bfc5a752d3f39c8cab9fc81e55b83 I guess

ejgallego commented 4 years ago

Oh, that's indeed incorrect, I didn't notice in the review, thanks for the pointer; I wonder why it fails but the support for native is not so easy as coqc will likely need some extra include paths, see https://github.com/ocaml/dune/pull/3210

ejgallego commented 4 years ago

Bignums + dune should be disabled for now; I was under the impression the opam package had gone back to Coq Makefile tho.

proux01 commented 4 years ago

Maybe because https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packages/coq-bignums/coq-bignums.dev/opam

I'm opening a PR on opam-coq-archive.