diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/ci-basic-overlay.sh | 4 | ||||
| -rwxr-xr-x | dev/ci/ci-vst.sh | 2 | ||||
| -rw-r--r-- | dev/doc/changes.txt | 10 |
3 files changed, 13 insertions, 3 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 91337b9013..6560305433 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -79,8 +79,8 @@ ######################################################################## # VST ######################################################################## -: ${VST_CI_BRANCH:=less_init_plugins} -: ${VST_CI_GITURL:=https://github.com/letouzey/VST.git} +: ${VST_CI_BRANCH:=master} +: ${VST_CI_GITURL:=https://github.com/Zimmi48/VST.git} ######################################################################## # fiat_parsers diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 27a336d80c..5bfc408e96 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -10,4 +10,4 @@ git_checkout ${VST_CI_BRANCH} ${VST_CI_GITURL} ${VST_CI_DIR} # Targets are: msl veric floyd # Patch to avoid the upper version limit -( cd ${VST_CI_DIR} && sed -i.bak 's/8.6$/8.6 or-else trunk/' Makefile && make ) +( cd ${VST_CI_DIR} && make IGNORECOQVERSION=true ) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index c3c86ac5c5..57c7a97d58 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -28,6 +28,16 @@ Coq is compiled with -safe-string enabled and requires plugins to do the same. This means that code using `String` in an imperative way will fail to compile now. They should switch to `Bytes.t` +* Plugin API * + +Coq 8.7 offers a new module overlay containing a proposed plugin API +in `API/API.ml`; this overlay is enabled by adding the `-open API` +flag to the OCaml compiler; this happens automatically for +developments in the `plugin` folder and `coq_makefile`. + +However, `coq_makefile` can be instructed not to enable this flag by +passing `-bypass-API`. + * ML API * Added two functions for declaring hooks to be executed in reduction |