Skip to content

[coq.dev] depends on zarith#1410

Merged
RalfJung merged 2 commits intorocq-prover:masterfrom
liyishuai:zarith
Aug 29, 2020
Merged

[coq.dev] depends on zarith#1410
RalfJung merged 2 commits intorocq-prover:masterfrom
liyishuai:zarith

Conversation

@liyishuai
Copy link
Copy Markdown
Member

@liyishuai liyishuai commented Aug 29, 2020

Comment thread core-dev/packages/coq/coq.dev/opam Outdated
Co-authored-by: Ralf Jung <post@ralfj.de>
@RalfJung
Copy link
Copy Markdown
Contributor

@ejgallego which version of ZArith does Coq need? The docs say 1.8, the opam file says 1.9.1.

@erikmd
Copy link
Copy Markdown
Contributor

erikmd commented Aug 29, 2020

Also, shouldn't the "num" dependency be removed as well?

@erikmd
Copy link
Copy Markdown
Contributor

erikmd commented Aug 29, 2020

On second thought, rocq-prover/rocq#11742 says We thus keep the num library linked for now until micromega is ported., so forget my previous comment…

@erikmd
Copy link
Copy Markdown
Contributor

erikmd commented Aug 29, 2020

@RalfJung

which version of ZArith does Coq need? The docs say 1.8, the opam file says 1.9.1.

it seems there is no version 1.8 available in opam-repository:

$ opam show zarith
<><> zarith: information on all versions ><><><><><><><><><><><><><><><><><><><>
name                   zarith
[…]
all-versions           1.1  1.2  1.3  1.4  1.4.1  1.5  1.6  1.7  1.7-1  1.9.1

@RalfJung
Copy link
Copy Markdown
Contributor

it seems there is no version 1.8 available in opam-repository:

Interesting.
That would make >= 1.8 work though... but I guess let's keep this consistent with the file in the Coq repo.

@RalfJung RalfJung merged commit 7763d84 into rocq-prover:master Aug 29, 2020
@liyishuai liyishuai deleted the zarith branch August 29, 2020 19:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

coq.dev compilation fails

3 participants