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

[core-dev] Rename coq-stdlib -> rocq-stdlib #3275

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

[core-dev] Rename coq-stdlib -> rocq-stdlib #3275

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions core-dev/packages/coq-stdlib/coq-stdlib.dev/opam
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
opam-version: "2.0"
synopsis: "The Coq Proof Assistant -- Standard Library"
synopsis: "Compatibility metapackage for Coq Stdlib library after the Rocq renaming"
description: """
Coq is a formal proof management system. It provides
a formal language to write mathematical definitions, executable
Expand All @@ -22,8 +22,8 @@ doc: "https://coq.github.io/doc/"
bug-reports: "https://github.com/coq/coq/issues"
depends: [
"dune" {>= "3.8"}
"rocq-runtime"
"rocq-core" {= version}
"coq-core"
"rocq-stdlib" {= version}
"odoc" {with-doc}
]
depopts: ["coq-native"]
Expand Down
51 changes: 51 additions & 0 deletions core-dev/packages/rocq-stdlib/rocq-stdlib.dev/opam
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
opam-version: "2.0"
synopsis: "The Rocq Proof Assistant -- Standard Library"
proux01 marked this conversation as resolved.
Show resolved Hide resolved
description: """
Rocq is a formal proof management system. It provides
a formal language to write mathematical definitions, executable
algorithms and theorems together with an environment for
semi-interactive development of machine-checked proofs.

Typical applications include the certification of properties of
programming languages (e.g. the CompCert compiler certification
project, or the Bedrock verified low-level programming library), the
formalization of mathematics (e.g. the full formalization of the
Feit-Thompson theorem or homotopy type theory) and teaching.

This package includes the Rocq Standard Library, that is to say, the
set of modules usually bound to the Stdlib.* namespace."""
maintainer: ["The Rocq standard library development team"]
authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
license: "LGPL-2.1-only"
homepage: "https://coq.inria.fr/"
doc: "https://coq.github.io/doc/"
bug-reports: "https://github.com/coq/coq/issues"
depends: [
"dune" {>= "3.8"}
"rocq-runtime"
"rocq-core" {= version}
"odoc" {with-doc}
]
depopts: ["coq-native"]
dev-repo: "git+https://github.com/coq/coq.git"
build: [
["sh" "-c" "echo '(dirs stdlib)' > dune"]
["dune" "subst"] {dev}
[
"stdlib/dev/with-rocq-wrap.sh"
"dune"
"build"
"-p"
name
"-j"
jobs
"@install"
"@runtest" {with-test}
"@doc" {with-doc}
]
["mv" "stdlib/rocq-stdlib.install" "."]
]

url {
src: "git+https://github.com/coq/coq.git#master"
}
Loading