Skip to content

Add 8.10 support / testing.#76

Merged
Zimmi48 merged 1 commit into
rocq-community:masterfrom
Zimmi48:test-8.10
Aug 20, 2019
Merged

Add 8.10 support / testing.#76
Zimmi48 merged 1 commit into
rocq-community:masterfrom
Zimmi48:test-8.10

Conversation

@Zimmi48
Copy link
Copy Markdown
Member

@Zimmi48 Zimmi48 commented Jul 13, 2019

Update to the latest versions of template, and switch opam files to 2.0.

@Zimmi48
Copy link
Copy Markdown
Member Author

Zimmi48 commented Jul 14, 2019

The new 8.10 testing does not work because there is no released version of math-classes that is compatible with Coq 8.10. See rocq-community/math-classes#74.

@Zimmi48
Copy link
Copy Markdown
Member Author

Zimmi48 commented Jul 17, 2019

@erikmd Can you help me understand the issue here? I added a test with the Coq 8.10 Docker image, and it fails in the following way:

+ (/bin/bash @ line 6) $ opam pin add coq-corn . -y -n -k path
[coq-corn.dev: rsync]
[coq-corn.dev] synchronised from file:///home/coq/coq-corn
coq-corn is now pinned to file:///home/coq/coq-corn (version dev)
+ (/bin/bash @ line 7) $ opam install coq-corn -y -j 2 --deps-only
<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
[coq-corn.dev] no changes from file:///home/coq/coq-corn
The following dependencies couldn't be met:
  - coq-corn -> coq >= dev
      not available because the package is pinned to version 8.10+beta2
No solution found, exiting

This seems weird: the opam file gives the following constraint on Coq:

   "coq" {(>= "8.6" & < "8.11~") | (= "dev")}

I would have thought that it would pick 8.10+beta2 has a version of Coq satisfying this constraint...

@erikmd
Copy link
Copy Markdown
Member

erikmd commented Jul 17, 2019

Hi @Zimmi48, I think this is because you named the .opam file corn.opam instead of coq-corn.opam, so when the install is requested, opam finds the wrong specification (namely that of the repo extra-dev, which is loaded in the coqorg/coq:8.10 image currently because 8.10 is a pre-release).

Copy link
Copy Markdown
Member Author

Zimmi48 commented Jul 17, 2019

Right my bad! Thanks a lot.

@Zimmi48
Copy link
Copy Markdown
Member Author

Zimmi48 commented Jul 17, 2019

It looks like it worked.

@Zimmi48
Copy link
Copy Markdown
Member Author

Zimmi48 commented Aug 20, 2019

Looks like we forgot to merge this.

@Zimmi48 Zimmi48 merged commit eeacb41 into rocq-community:master Aug 20, 2019
@Zimmi48 Zimmi48 deleted the test-8.10 branch August 20, 2019 07:43
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.

2 participants