aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/nix/default.nix16
-rw-r--r--dev/ci/nix/iris.nix4
-rw-r--r--dev/ci/nix/lambda-rust.nix4
-rw-r--r--dev/ci/nix/unicoq/META2
-rw-r--r--dev/ci/nix/unicoq/default.nix11
-rw-r--r--dev/core_dune.dbg2
-rw-r--r--doc/README.md6
-rw-r--r--test-suite/stm/arg_filter_1.v4
-rw-r--r--toplevel/coqargs.ml38
9 files changed, 63 insertions, 24 deletions
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index 277e9ee08f..94e0a666e2 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -39,11 +39,21 @@ let corn = (coqPackages.corn.override { inherit coq bignums math-classes; })
src = fetchTarball "https://github.com/coq-community/corn/archive/master.tar.gz";
}); in
+let stdpp = coqPackages.stdpp.overrideAttrs (o: {
+ src = fetchTarball "https://gitlab.mpi-sws.org/iris/stdpp/-/archive/master/stdpp-master.tar.bz2";
+ }); in
+
+let iris = (coqPackages.iris.override { inherit coq stdpp; })
+ .overrideAttrs (o: {
+ src = fetchTarball "https://gitlab.mpi-sws.org/iris/iris/-/archive/master/iris-master.tar.bz2";
+ propagatedBuildInputs = [ stdpp ];
+ }); in
+
let unicoq = callPackage ./unicoq { inherit coq; }; in
let callPackage = newScope { inherit coq
- bignums coq-ext-lib coqprime corn math-classes
- mathcomp simple-io ssreflect unicoq;
+ bignums coq-ext-lib coqprime corn iris math-classes
+ mathcomp simple-io ssreflect stdpp unicoq;
}; in
# Environments for building CI libraries with this Coq
@@ -62,6 +72,8 @@ let projects = {
formal-topology = callPackage ./formal-topology.nix {};
GeoCoq = callPackage ./GeoCoq.nix {};
HoTT = callPackage ./HoTT.nix {};
+ iris = callPackage ./iris.nix {};
+ lambda-rust = callPackage ./lambda-rust.nix {};
math_classes = callPackage ./math_classes.nix {};
mathcomp = {};
mtac2 = callPackage ./mtac2.nix {};
diff --git a/dev/ci/nix/iris.nix b/dev/ci/nix/iris.nix
new file mode 100644
index 0000000000..b55cccc7c6
--- /dev/null
+++ b/dev/ci/nix/iris.nix
@@ -0,0 +1,4 @@
+{ stdpp }:
+{
+ coqBuildInputs = [ stdpp ];
+}
diff --git a/dev/ci/nix/lambda-rust.nix b/dev/ci/nix/lambda-rust.nix
new file mode 100644
index 0000000000..0d07c3028a
--- /dev/null
+++ b/dev/ci/nix/lambda-rust.nix
@@ -0,0 +1,4 @@
+{ iris }:
+{
+ coqBuildInputs = [ iris ];
+}
diff --git a/dev/ci/nix/unicoq/META b/dev/ci/nix/unicoq/META
deleted file mode 100644
index 30dd8b5559..0000000000
--- a/dev/ci/nix/unicoq/META
+++ /dev/null
@@ -1,2 +0,0 @@
-archive(native) = "unicoq.cmxa"
-plugin(native) = "unicoq.cmxs"
diff --git a/dev/ci/nix/unicoq/default.nix b/dev/ci/nix/unicoq/default.nix
index 36f40dbe33..54c67ac0fd 100644
--- a/dev/ci/nix/unicoq/default.nix
+++ b/dev/ci/nix/unicoq/default.nix
@@ -1,4 +1,10 @@
-{ stdenv, coq }:
+{ stdenv, writeText, coq }:
+
+let META = writeText "META" ''
+ archive(native) = "unicoq.cmxa"
+ plugin(native) = "unicoq.cmxs"
+''; in
+
stdenv.mkDerivation {
name = "coq${coq.coq-version}-unicoq-0.0-git";
@@ -12,8 +18,9 @@ stdenv.mkDerivation {
installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
postInstall = ''
+ cp ${META} META
install -d $OCAMLFIND_DESTDIR
ln -s $out/lib/coq/${coq.coq-version}/user-contrib/Unicoq $OCAMLFIND_DESTDIR/
- install -m 0644 ${./META} src/unicoq.a $OCAMLFIND_DESTDIR/Unicoq
+ install -m 0644 META src/unicoq.a $OCAMLFIND_DESTDIR/Unicoq
'';
}
diff --git a/dev/core_dune.dbg b/dev/core_dune.dbg
index cf9c5bd39a..4e1035f7b6 100644
--- a/dev/core_dune.dbg
+++ b/dev/core_dune.dbg
@@ -1,10 +1,10 @@
load_printer threads.cma
load_printer str.cma
-load_printer gramlib.cma
load_printer config.cma
load_printer clib.cma
load_printer dynlink.cma
load_printer lib.cma
+load_printer gramlib.cma
load_printer byterun.cma
load_printer kernel.cma
load_printer library.cma
diff --git a/doc/README.md b/doc/README.md
index c41d269437..b784fe92f6 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -9,8 +9,10 @@ The Coq documentation includes
The documentation of the latest released version is available on the Coq
web site at [coq.inria.fr/documentation](http://coq.inria.fr/documentation).
-Additionally, you can view the documentation for the current master version at
-<https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman>.
+Additionally, you can view the reference manual for the development version
+at <https://coq.github.io/doc/master/refman/>, and the documentation of the
+standard library for the development version at
+<https://coq.github.io/doc/master/stdlib/>.
The reference manual is written is reStructuredText and compiled
using Sphinx. See [`sphinx/README.rst`](sphinx/README.rst)
diff --git a/test-suite/stm/arg_filter_1.v b/test-suite/stm/arg_filter_1.v
index 1cf66d6b43..ed87d67405 100644
--- a/test-suite/stm/arg_filter_1.v
+++ b/test-suite/stm/arg_filter_1.v
@@ -1,4 +1,4 @@
(* coq-prog-args: ("-async-proofs-tac-j" "1") *)
-Lemma foo : True.
-Proof. now auto. Qed.
+Lemma foo (A B : Prop) n : n + 0 = n /\ (A -> B -> A).
+Proof. split. par: now auto. Qed.
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index b549f22119..c110f3831e 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -13,6 +13,9 @@ let fatal_error exn =
let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in
exit exit_code
+let error_wrong_arg msg =
+ prerr_endline msg; exit 1
+
let error_missing_arg s =
prerr_endline ("Error: extra argument expected after option "^s);
prerr_endline "See -help for the syntax of supported options";
@@ -169,7 +172,8 @@ let set_color opts = function
| "yes" | "on" -> { opts with color = `ON }
| "no" | "off" -> { opts with color = `OFF }
| "auto" -> { opts with color = `AUTO }
-| _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1
+| _ ->
+ error_wrong_arg ("Error: on/off/auto expected after option color")
let warn_deprecated_inputstate =
CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
@@ -187,26 +191,26 @@ let exitcode opts = if opts.filter_opts then 2 else 0
let get_bool opt = function
| "yes" | "on" -> true
| "no" | "off" -> false
- | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1
+ | _ ->
+ error_wrong_arg ("Error: yes/no expected after option "^opt)
let get_int opt n =
try int_of_string n
with Failure _ ->
- prerr_endline ("Error: integer expected after option "^opt); exit 1
+ error_wrong_arg ("Error: integer expected after option "^opt)
let get_float opt n =
try float_of_string n
with Failure _ ->
- prerr_endline ("Error: float expected after option "^opt); exit 1
+ error_wrong_arg ("Error: float expected after option "^opt)
let get_host_port opt s =
match String.split_on_char ':' s with
| [host; portr; portw] ->
- Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
+ Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
| ["stdfds"] -> Some Spawned.AnonPipe
| _ ->
- prerr_endline ("Error: host:portr:portw or stdfds expected after option "^opt);
- exit 1
+ error_wrong_arg ("Error: host:portr:portw or stdfds expected after option "^opt)
let get_error_resilience opt = function
| "on" | "all" | "yes" -> `All
@@ -216,17 +220,20 @@ let get_error_resilience opt = function
let get_priority opt s =
try CoqworkmgrApi.priority_of_string s
with Invalid_argument _ ->
- prerr_endline ("Error: low/high expected after "^opt); exit 1
+ error_wrong_arg ("Error: low/high expected after "^opt)
let get_async_proofs_mode opt = let open Stm.AsyncOpts in function
| "no" | "off" -> APoff
| "yes" | "on" -> APon
| "lazy" -> APonLazy
- | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1
+ | _ ->
+ error_wrong_arg ("Error: on/off/lazy expected after "^opt)
let get_cache opt = function
| "force" -> Some Stm.AsyncOpts.Force
- | _ -> prerr_endline ("Error: force expected after "^opt); exit 1
+ | _ ->
+ error_wrong_arg ("Error: force expected after "^opt)
+
let get_native_name s =
(* We ignore even critical errors because this mode has to be super silent *)
@@ -311,8 +318,12 @@ let parse_args ~help ~init arglist : t * string list =
}}
|"-async-proofs-tac-j" ->
+ let j = get_int opt (next ()) in
+ if j <= 0 then begin
+ error_wrong_arg ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1")
+ end;
{ oval with stm_flags = { oval.stm_flags with
- Stm.AsyncOpts.async_proofs_n_tacworkers = (get_int opt (next ()))
+ Stm.AsyncOpts.async_proofs_n_tacworkers = j
}}
|"-async-proofs-worker-priority" ->
@@ -431,7 +442,8 @@ let parse_args ~help ~init arglist : t * string list =
| ("yes" | "on") -> NativeOn {ondemand=false}
| "ondemand" -> NativeOn {ondemand=true}
| ("no" | "off") -> NativeOff
- | _ -> prerr_endline ("Error: (yes|no|ondemand) expected after option -native-compiler"); exit 1
+ | _ ->
+ error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler")
in
{ oval with native_compiler }
@@ -456,7 +468,7 @@ let parse_args ~help ~init arglist : t * string list =
if List.exists (fun x -> opt = x) ["off"; "on"; "removed"] then
Proof_diffs.write_diffs_option opt
else
- (prerr_endline ("Error: on|off|removed expected after -diffs"); exit 1);
+ error_wrong_arg "Error: on|off|removed expected after -diffs";
{ oval with diffs_set = true }
|"-stm-debug" -> Stm.stm_debug := true; oval
|"-emacs" -> set_emacs oval
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 03:33:20 +0000