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.

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

coq: 8.19.1 → 8.19.2 #318799

Merged
merged 2 commits into from
Jun 17, 2024
Merged

coq: 8.19.1 → 8.19.2 #318799

merged 2 commits into from
Jun 17, 2024

Conversation

vbgl
Copy link
Contributor

@vbgl vbgl commented Jun 10, 2024

Description of changes

https://coq.inria.fr/doc/V8.19.2/refman/changes.html#changes-in-8-19-2

Tested there: coq-community/coq-nix-toolbox#223

Things done

  • Built on platform(s)
    • x86_64-linux
    • aarch64-linux
    • x86_64-darwin
    • aarch64-darwin
  • For non-Linux: Is sandboxing enabled in nix.conf? (See Nix manual)
    • sandbox = relaxed
    • sandbox = true
  • Tested, as applicable:
  • Tested compilation of all packages that depend on this change using nix-shell -p nixpkgs-review --run "nixpkgs-review rev HEAD". Note: all changes have to be committed, also see nixpkgs-review usage
  • Tested basic functionality of all binary files (usually in ./result/bin/)
  • 24.11 Release Notes (or backporting 23.11 and 24.05 Release notes)
    • (Package updates) Added a release notes entry if the change is major or breaking
    • (Module updates) Added a release notes entry if the change is significant
    • (Module addition) Added a release notes entry if adding a new NixOS module
  • Fits CONTRIBUTING.md.

Add a 👍 reaction to pull requests you find important.

@vbgl vbgl added 8.has: package (update) This PR updates a package to a newer version 6.topic: coq "A formal proof management system" backport release-24.05 labels Jun 10, 2024
@Alizter
Copy link
Contributor

Alizter commented Jun 10, 2024

There is now an optional dependency on memprof-limits. Should we add this as a dependency for versions > 8.19.2? I've added memprof-limits here: #318800

@ofborg ofborg bot added 11.by: package-maintainer This PR was created by the maintainer of the package it changes 10.rebuild-darwin: 11-100 10.rebuild-linux: 11-100 labels Jun 10, 2024
@vbgl
Copy link
Contributor Author

vbgl commented Jun 11, 2024

Can you please elaborate on this new (optional) dependency? Should it be opt-in or opt-out for nixpkgs users?

@Alizter
Copy link
Contributor

Alizter commented Jun 11, 2024

I think for the time being lets ignore it. We will need to think a bit harder about how we want to depend on it in the future.

@siraben

This comment has been minimized.

@siraben
Copy link
Member

siraben commented Jun 15, 2024

Result of nixpkgs-review pr 318799 run on x86_64-linux 1

72 packages built:
  • compcert (coqPackages.compcert)
  • compcert.doc (coqPackages.compcert.doc)
  • compcert.lib (coqPackages.compcert.lib)
  • compcert.man (coqPackages.compcert.man)
  • coq (coqPackages.coq ,coq_8_19)
  • coqPackages.Cheerios
  • coqPackages.CoLoR
  • coqPackages.HoTT
  • coqPackages.ITree
  • coqPackages.InfSeqExt
  • coqPackages.LibHyps
  • coqPackages.QuickChick
  • coqPackages.StructTact
  • coqPackages.VST
  • coqPackages.aac-tactics
  • coqPackages.bignums
  • coqPackages.ceres
  • coqPackages.coq-elpi
  • coqPackages.coq-ext-lib
  • coqPackages.coq-lsp
  • coqPackages.coq-record-update
  • coqPackages.coqide
  • coqPackages.coqprime
  • coqPackages.coquelicot
  • coqPackages.corn
  • coqPackages.deriving
  • coqPackages.dpdgraph
  • coqPackages.equations
  • coqPackages.extructures
  • coqPackages.flocq
  • coqPackages.fourcolor
  • coqPackages.gappalib
  • coqPackages.hierarchy-builder
  • coqPackages.interval
  • coqPackages.iris
  • coqPackages.iris-named-props
  • coqPackages.itauto
  • coqPackages.math-classes
  • coqPackages.mathcomp
  • coqPackages.mathcomp-algebra
  • coqPackages.mathcomp-algebra-tactics
  • coqPackages.mathcomp-analysis
  • coqPackages.mathcomp-bigenough
  • coqPackages.mathcomp-character
  • coqPackages.mathcomp-classical
  • coqPackages.mathcomp-field
  • coqPackages.mathcomp-fingroup
  • coqPackages.mathcomp-finmap
  • coqPackages.mathcomp-infotheo
  • coqPackages.mathcomp-real-closed
  • coqPackages.mathcomp-solvable
  • coqPackages.ssreflect (coqPackages.mathcomp-ssreflect)
  • coqPackages.mathcomp-word
  • coqPackages.mathcomp-zify
  • coqPackages.metacoq
  • coqPackages.metacoq-erasure
  • coqPackages.metacoq-pcuic
  • coqPackages.metacoq-safechecker
  • coqPackages.metacoq-template-coq
  • coqPackages.multinomials
  • coqPackages.paco
  • coqPackages.paramcoq
  • coqPackages.parsec
  • coqPackages.reglang
  • coqPackages.serapi
  • coqPackages.simple-io
  • coqPackages.stdpp
  • coqPackages.vcfloat
  • coqPackages.vscoq-language-server
  • coqPackages.zorns-lemma
  • framac
  • satallax

@vbgl vbgl merged commit f7ff7d4 into NixOS:master Jun 17, 2024
30 checks passed
@vbgl vbgl deleted the coq-8.19.2 branch June 17, 2024 07:15
Copy link
Contributor

Successfully created backport PR for release-24.05:

vbgl added a commit to vbgl/coq-nix-toolbox that referenced this pull request Jun 17, 2024
vbgl added a commit to vbgl/coq-nix-toolbox that referenced this pull request Jun 17, 2024
vbgl added a commit to coq-community/coq-nix-toolbox that referenced this pull request Jun 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
6.topic: coq "A formal proof management system" 8.has: package (update) This PR updates a package to a newer version 10.rebuild-darwin: 11-100 10.rebuild-linux: 11-100 11.by: package-maintainer This PR was created by the maintainer of the package it changes
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants