diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/ci-basic-overlay.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-iris-lambda-rust.sh | 4 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06686-ccnv-no-proj.sh | 4 | ||||
| -rw-r--r-- | dev/doc/changes.md | 11 |
4 files changed, 18 insertions, 3 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 628e892910..784da6f971 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -70,7 +70,7 @@ # Flocq ######################################################################## : "${Flocq_CI_BRANCH:=master}" -: "${Flocq_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git}" +: "${Flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq.git}" ######################################################################## # Coquelicot diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh index cf24d202d9..267e13359b 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -34,8 +34,8 @@ git_checkout ${stdpp_CI_BRANCH} ${stdpp_URL_PARTS[0]} ${stdpp_CI_DIR} ${stdpp_UR # Build std++ ( cd ${stdpp_CI_DIR} && make && make install ) -# Build iris -( cd ${Iris_CI_DIR} && make && make install ) +# Build and validate (except on Travis, i.e., skip if TRAVIS is non-empty) Iris +( cd ${Iris_CI_DIR} && make && (test -n "${TRAVIS}" || make validate) && make install ) # Build lambdaRust ( cd ${lambdaRust_CI_DIR} && make && make install ) diff --git a/dev/ci/user-overlays/06686-ccnv-no-proj.sh b/dev/ci/user-overlays/06686-ccnv-no-proj.sh new file mode 100644 index 0000000000..3a3ab44e03 --- /dev/null +++ b/dev/ci/user-overlays/06686-ccnv-no-proj.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "6686" ] || [ "$CI_BRANCH" = "ccnv-no-proj" ]; then + Equations_CI_BRANCH=ccnv-fixes + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index e616bd5663..aef62b0092 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -58,6 +58,17 @@ Declaration of printers for arguments used only in vernac command happen. An alternative is to register the corresponding argument as a value, using "Geninterp.register_val0 wit None". +### STM API + +The STM API has seen a general overhaul. The main change is the +introduction of a "Coq document" type, which all operations now take +as a parameter. This effectively functionalize the STM API and will +allow in the future to handle several documents simultaneously. + +The main remarkable point is that key implicit global parameters such +as load-paths and required modules are now arguments to the document +creation function. This helps enforcing some key invariants. + ### XML IDE Protocol - Before 8.8, `Query` only executed the first command present in the |