aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/build/windows/ReadMe.txt2
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh16
-rwxr-xr-xdev/ci/ci-basic-overlay.sh2
-rwxr-xr-xdev/ci/ci-fiat_crypto.sh4
-rwxr-xr-xdev/ci/ci-fiat_crypto_ocaml.sh8
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile5
-rw-r--r--dev/doc/critical-bugs10
-rw-r--r--dev/include_printers1
-rw-r--r--dev/top_printers.dbg1
-rw-r--r--dev/top_printers.ml1
-rw-r--r--dev/top_printers.mli1
11 files changed, 32 insertions, 19 deletions
diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt
index 052014824f..f34bbea4e9 100644
--- a/dev/build/windows/ReadMe.txt
+++ b/dev/build/windows/ReadMe.txt
@@ -423,7 +423,7 @@ Binary file ./bin/ocpp5.exe matches
Binary file ./lib/config/coq_config.cmo matches
Binary file ./lib/config/coq_config.o matches
Binary file ./lib/grammar/grammar.cma matches
-Binary file ./lib/ide/ide_win32_stubs.o matches
+Binary file ./lib/ide/coqide/ide_win32_stubs.o matches
Binary file ./lib/lib/clib.a matches
Binary file ./lib/lib/clib.cma matches
Binary file ./lib/libcoqrun.a matches
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 963b0e6387..4a6555a4f7 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1303,11 +1303,11 @@ function copy_coq_gtk {
install -D -T "$PREFIXMINGW/share/glib-2.0/schemas/gschemas.compiled" "$PREFIXCOQ/share/glib-2.0/schemas/gschemas.compiled"
install_glob "$PREFIXMINGW/share/gtksourceview-3.0/language-specs" '*' "$PREFIXCOQ/share/gtksourceview-3.0/language-specs"
- install -D -T "ide/coq.lang" "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq.lang"
- install -D -T "ide/coq-ssreflect.lang" "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq-ssreflect.lang"
+ install -D -T "ide/coqide/coq.lang" "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq.lang"
+ install -D -T "ide/coqide/coq-ssreflect.lang" "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq-ssreflect.lang"
install_glob "$PREFIXMINGW/share/gtksourceview-3.0/styles" '*' "$PREFIXCOQ/share/gtksourceview-3.0/styles"
- install -D -T "ide/coq_style.xml" "$PREFIXCOQ/share/gtksourceview-3.0/styles/coq_style.xml"
+ install -D -T "ide/coqide/coq_style.xml" "$PREFIXCOQ/share/gtksourceview-3.0/styles/coq_style.xml"
install_rec "$PREFIXMINGW/share/themes" '*' "$PREFIXCOQ/share/themes"
@@ -1340,8 +1340,8 @@ function copy_coq_gtk {
# COQSHARE="$PREFIXCOQ/share/"
# fi
- # mkdir -p "$PREFIXCOQ/ide"
- # mv "$COQSHARE"*.png "$PREFIXCOQ/ide"
+ # mkdir -p "$PREFIXCOQ/ide/coqide"
+ # mv "$COQSHARE"*.png "$PREFIXCOQ/ide/coqide"
# rmdir "$PREFIXCOQ/share/coq" || true
fi
}
@@ -1598,7 +1598,7 @@ function make_coq_installer {
cp ../patches/ReplaceInFile.nsh dev/nsis
VERSION=$(grep '^VERSION=' config/Makefile | cut -d = -f 2 | tr -d '\r')
cd dev/nsis
- logn nsis-installer "$NSIS" -DVERSION="$VERSION" -DARCH="$ARCH" -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi
+ logn nsis-installer "$NSIS" -DVERSION="$VERSION" -DARCH="$ARCH" -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coqide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi
build_post
fi
@@ -1880,9 +1880,9 @@ function make_addon_quickchick {
# Flocq: Floating point library
function make_addon_flocq {
- if build_prep_overlay Flocq; then
+ if build_prep_overlay flocq; then
installer_addon_section flocq "Flocq" "Coq library for floating point arithmetic" ""
- logn autogen ./autogen.sh
+ log1 autoconf
logn configure ./configure
logn remake ./remake --jobs=$MAKE_THREADS
logn install ./remake install
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 19ba9de245..4ebc637a68 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -31,7 +31,7 @@
########################################################################
# Unicoq + Mtac2
########################################################################
-: "${unicoq_CI_REF:=master}"
+: "${unicoq_CI_REF:=68ed13294ea8860a8c39950f7ca2ff0aa7211b9f}"
: "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}"
: "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-fiat_crypto.sh b/dev/ci/ci-fiat_crypto.sh
index 811fefda35..3ecdb32a51 100755
--- a/dev/ci/ci-fiat_crypto.sh
+++ b/dev/ci/ci-fiat_crypto.sh
@@ -15,8 +15,8 @@ fiat_crypto_CI_STACKSIZE=32768
# bedrock2, so we use the pinned version of bedrock2, but the external
# version of other developments
fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1"
-fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml c-files rust-files printlite lite"
-fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all"
+fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} pre-standalone-extracted printlite lite"
+fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all-except-compiled"
( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
ulimit -s ${fiat_crypto_CI_STACKSIZE} && \
diff --git a/dev/ci/ci-fiat_crypto_ocaml.sh b/dev/ci/ci-fiat_crypto_ocaml.sh
new file mode 100755
index 0000000000..20d3deb14f
--- /dev/null
+++ b/dev/ci/ci-fiat_crypto_ocaml.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1"
+
+( cd "${CI_BUILD_DIR}/fiat_crypto" && make ${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml lite-generated-files )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 0d2f1dfbc7..8c5696f4f9 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-05-19-V33"
+# CACHEKEY: "bionic_coq-V2020-05-24-V1"
# ^^ Update when modifying this file.
FROM ubuntu:bionic
@@ -13,8 +13,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
libgtksourceview-3.0-dev \
# Dependencies of stdlib and sphinx doc
texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \
- xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \
- fonts-freefont-otf \
+ python3-pip python3-setuptools python3-pexpect python3-bs4 fonts-freefont-otf \
# Dependencies of source-doc and coq-makefile
texlive-science tipa
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 3260040248..066facd5db 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -347,6 +347,16 @@ Conflicts with axioms in library
GH issue number: none
risk:
+ component: primitive floating-points
+ summary: Incorrect specification of PrimFloat.leb
+ introduced: 8.11
+ impacted released versions: 8.11.0, 8.11.1, 8.11.2
+ fixed by fixing the spec: #12484
+ found by: Pierre Roux
+ exploit: test-suite/bugs/closed/bug_12483.v
+ GH issue number: #12483
+ risk: proof of false when using the incorrect axiom
+
There were otherwise several bugs in beta-releases, from memory, bugs with beta versions of primitive projections or template polymorphism or native compilation or guard (e7fc96366, 2a4d714a1).
There were otherwise maybe unexploitable kernel bugs, e.g. 2df88d83 (Require overloading), 0adf0838 ("Univs: uncovered bug in strengthening of opaque polymorphic definitions."), 5122a398 (#3746 about functors), #4346 (casts in VM), a14bef4 (guard condition in 8.1), 6ed40a8 ("Georges' bug" with ill-typed lazy machine), and various other bugs in 8.0 or 8.1 w/o knowing if they are critical.
diff --git a/dev/include_printers b/dev/include_printers
index d077075eeb..30529b5fd6 100644
--- a/dev/include_printers
+++ b/dev/include_printers
@@ -27,7 +27,6 @@
#install_printer (* id set *) ppidset;;
#install_printer (* int set *) ppintset;;
-#install_printer (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;;
#install_printer (* Reductionops machine stack *) pp_stack_t;;
(*#install_printer (* hint_db *) print_hint_db;;*)
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index 06db787488..63071bba72 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -46,7 +46,6 @@ install_printer Top_printers.pp_idpred
install_printer Top_printers.pp_cpred
install_printer Top_printers.pp_transparent_state
install_printer Top_printers.pp_stack_t
-install_printer Top_printers.pp_cst_stack_t
install_printer Top_printers.pp_state_t
install_printer Top_printers.ppmetas
install_printer Top_printers.ppevm
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 00050a89e1..bca1eb5754 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -169,7 +169,6 @@ let pp_idpred s = pp (pr_idpred s)
let pp_cpred s = pp (pr_cpred s)
let pp_transparent_state s = pp (pr_transparent_state s)
let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> pr_econstr) n)
-let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr Global.(env()) Evd.empty n)
let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty n)
(* proof printers *)
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index c826391cac..65eab8daa3 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -106,7 +106,6 @@ val pp_cpred : Names.Cpred.t -> unit
val pp_transparent_state : TransparentState.t -> unit
val pp_stack_t : Constr.t Reductionops.Stack.t -> unit
-val pp_cst_stack_t : Reductionops.Cst_stack.t -> unit
val pp_state_t : Reductionops.state -> unit
val ppmetas : Evd.Metaset.t -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 19:28:29 +0000