aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh2
-rw-r--r--dev/ci/README-developers.md21
-rwxr-xr-xdev/ci/ci-basic-overlay.sh6
-rwxr-xr-xdev/ci/ci-cpdt.sh9
-rwxr-xr-xdev/ci/ci-tlc.sh9
-rw-r--r--dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh6
-rw-r--r--dev/ci/user-overlays/10665-ejgallego-api+varkind.sh9
-rw-r--r--dev/doc/build-system.dune.md8
-rw-r--r--dev/nixpkgs.nix4
9 files changed, 37 insertions, 37 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 0c8213b8f5..78c0b4b2c7 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1132,7 +1132,7 @@ function make_findlib {
function make_dune {
make_ocaml
- if build_prep https://github.com/ocaml/dune/archive/ 1.6.3 tar.gz 1 dune-1.6.3 ; then
+ if build_prep https://github.com/ocaml/dune/archive/ 1.10.0 tar.gz 1 dune-1.10.0 ; then
log2 make release
log2 make install
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 408d36df7f..9ed7180807 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -120,15 +120,18 @@ Currently available artifacts are:
Additionally, an experimental Dune build is provided:
https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune:dev
-- the Coq documentation, built in the `doc:*` jobs. When submitting
- a documentation PR, this can help reviewers checking the rendered result:
-
- + Coq's Reference Manual [master branch]
- https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman
- + Coq's Standard Library Documentation [master branch]
- https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=build:base
- + Coq's ML API Documentation [master branch]
- https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc
+- the Coq documentation, built in the `doc:*` jobs. When submitting a
+ documentation PR, this can help reviewers checking the rendered
+ result. **@coqbot** will automatically post links to these
+ artifacts in the PR checks section. Furthemore, these artifacts are
+ automatically deployed at:
+
+ + Coq's Reference Manual [master branch]:
+ <https://coq.github.io/doc/master/refman/>
+ + Coq's Standard Library Documentation [master branch]:
+ <https://coq.github.io/doc/master/stdlib/>
+ + Coq's ML API Documentation [master branch]:
+ <https://coq.github.io/doc/master/api/>
### GitLab and Windows
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index ad22c394d8..3923fea30e 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -56,14 +56,14 @@
# NB: stdpp and Iris refs are gotten from the opam files in the Iris
# and lambdaRust repos respectively.
-: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp}"
+: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/iris/stdpp}"
: "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}"
-: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq}"
+: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}"
: "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}"
: "${lambdaRust_CI_REF:=master}"
-: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq}"
+: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/iris/lambda-rust}"
: "${lambdaRust_CI_ARCHIVEURL:=${lambdaRust_CI_GITURL}/-/archive}"
########################################################################
diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh
deleted file mode 100755
index ca759c7b39..0000000000
--- a/dev/ci/ci-cpdt.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-wget http://adam.chlipala.net/cpdt/cpdt.tgz
-tar xvfz cpdt.tgz
-
-( cd cpdt && make clean && make )
diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
deleted file mode 100755
index a2f0bea555..0000000000
--- a/dev/ci/ci-tlc.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-FORCE_GIT=1
-git_download tlc
-
-( cd "${CI_BUILD_DIR}/tlc" && make )
diff --git a/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh b/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh
new file mode 100644
index 0000000000..413805e8e9
--- /dev/null
+++ b/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10642" ] || [ "$CI_BRANCH" = "feedback-added-axiom" ]; then
+
+ elpi_CI_REF=feedback-added-axiom
+ elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh b/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh
new file mode 100644
index 0000000000..0c47f6a60b
--- /dev/null
+++ b/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "10665" ] || [ "$CI_BRANCH" = "api+varkind" ]; then
+
+ elpi_CI_REF=api+varkind
+ elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+ quickchick_CI_REF=api+varkind
+ quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick
+
+fi
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 372e40a0b7..37c6e2f619 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -52,7 +52,7 @@ order to use them, do:
```
$ make -f Makefile.dune voboot # Only once per session
-$ dune exec dev/shim/coqtop-prelude
+$ dune exec -- dev/shim/coqtop-prelude
```
or `quickide` / `dev/shim/coqide-prelude` for CoqIDE. These targets
@@ -108,14 +108,14 @@ automatically.
You can use `ocamldebug` with Dune; after a build, do:
```
-dune exec dev/dune-dbg /path/to/foo.v
+dune exec -- dev/dune-dbg /path/to/foo.v
(ocd) source dune_db
```
or
```
-dune exec dev/dune-dbg checker Foo
+dune exec -- dev/dune-dbg checker Foo
(ocd) source dune_db
```
@@ -130,7 +130,7 @@ For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`.
After doing `make -f Makefile.dune voboot`, the following commands should work:
```
-dune exec dev/shim/coqbyte-prelude
+dune exec -- dev/shim/coqbyte-prelude
> Drop.
# #directory "dev";;
# #use "include_dune";;
diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix
index 8dfe1e7833..8736c0f9b8 100644
--- a/dev/nixpkgs.nix
+++ b/dev/nixpkgs.nix
@@ -1,4 +1,4 @@
import (fetchTarball {
- url = "https://github.com/NixOS/nixpkgs/archive/bc9df0f66110039e495b6debe3a6cda4a1bb0fed.tar.gz";
- sha256 = "0y2w259j0vqiwjhjvlbsaqnp1nl2zwz6sbwwhkrqn7k7fmhmxnq1";
+ url = "https://github.com/NixOS/nixpkgs/archive/31c38894c90429c9554eab1b416e59e3b6e054df.tar.gz";
+ sha256 = "1fv14rj5zslzm14ak4lvwqix94gm18h28376h4hsmrqqpnfqwsdw";
})