Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Coq update #27918

Merged
merged 4 commits into from Aug 4, 2017
Merged

Coq update #27918

merged 4 commits into from Aug 4, 2017

Conversation

Zimmi48
Copy link
Member

@Zimmi48 Zimmi48 commented Aug 3, 2017 •
edited

Motivation for this change

Mainly, an update of Coq to the latest patch-level release.
Also, two independent commits, one switching camlp5 to the strict mode (see commit message) and one adding myself as a maintainer of the Coq package.

Things done

Please check what applies. Note that these are not hard requirements but merely serve as information for reviewers.

  • Tested using sandboxing
    (nix.useSandbox on NixOS,
    or option build-use-sandbox in nix.conf
    on non-NixOS)
  • Built on platform(s)
    • NixOS
    • macOS
    • Linux
  • Tested via one or more NixOS test(s) if existing and applicable for the change (look inside nixos/tests)
  • Tested compilation of all pkgs that depend on this change using nix-shell -p nox --run "nox-review wip"
  • Tested execution of all binary files (usually in ./result/bin/)
  • Fits CONTRIBUTING.md.

@mention-bot
Copy link

@Zimmi48, thanks for your PR! By analyzing the history of the files in this pull request, we identified @vbgl, @zimbatm and @zraexy to be potential reviewers.

@Zimmi48
Copy link
Member Author

Zimmi48 commented Aug 3, 2017

Note that this cannot be merged as-is because it breaks CompCert:

Testing Coq... version 8.6.1 -- UNSUPPORTED
Error: CompCert requires Coq version 8.6.

This is fixed in CompCert's master branch though: AbsInt/CompCert@5547231

@vbgl
Copy link
Contributor

vbgl commented Aug 4, 2017

Thanks. BTW, CompCert seems to be already broken on master (https://hydra.nixos.org/job/nixpkgs/trunk/compcert.x86_64-linux): do you have any hint?

@Zimmi48
Copy link
Member Author

Zimmi48 commented Aug 4, 2017

Well, all I can say is that the faulty commit is @jwiegley's f130ecd. Most likely it was tested only on Darwin before being pushed.

@jwiegley
Copy link
Contributor

jwiegley commented Aug 4, 2017

I thought I had tested this in a Docker image, but apparently that slipped through the cracks. For Linux, just changing back to 32-bit should be fine.

@Zimmi48
Copy link
Member Author

Zimmi48 commented Aug 4, 2017

I thought I had tested this in a Docker image, but apparently that slipped through the cracks. For Linux, just changing back to 32-bit should be fine.

I'll add a commit doing that to this PR and I'll propose to pin the Coq version used by CompCert to 8.6 until the next release (which I just heard should be end of August).

@Zimmi48
Copy link
Member Author

Zimmi48 commented Aug 4, 2017

For CompCert I've actually found a much better fix. See 5215ed6.

So all in all, this PR should now be ready to go.

@Zimmi48
coq: 8.6 -> 8.6.1
c0dca2f
@Zimmi48
coq: use camlp5_strict
b25d65e 
The versions of Coq available through this expression do not actually
require camlp5_transitional. We drop this dependency to see if, in the
future, the package camlp5_transitional can be removed from nixpkgs.
@Zimmi48
coq: adding myself to the maintainers
057ffcf
@Zimmi48
Copy link
Member Author

Zimmi48 commented Aug 4, 2017

So Travis failed (because of a timeout on Linux, because of a broken dependency on Darwin, that must have been broken before this PR) but nox-review wip succeeds on my machine.

@jwiegley jwiegley merged commit 6ff50dc into NixOS:master Aug 4, 2017
@Zimmi48 Zimmi48 deleted the coq-update branch August 4, 2017 22:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@Zimmi48 @mention-bot @vbgl @jwiegley