aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.circleci/config.yml4
-rw-r--r--.gitlab-ci.yml3
-rw-r--r--.travis.yml6
-rw-r--r--Makefile.ci1
-rwxr-xr-xdev/ci/ci-basic-overlay.sh6
-rwxr-xr-xdev/ci/ci-cross-crypto.sh11
-rw-r--r--lib/coqProject_file.ml415
-rw-r--r--library/lib.ml19
-rwxr-xr-xtest-suite/coq-makefile/timing/run.sh2
-rwxr-xr-xtest-suite/misc/coqc_dash_o.sh15
-rw-r--r--test-suite/misc/coqc_dash_o.v1
-rw-r--r--tools/coqdep.ml53
-rw-r--r--tools/coqdep_common.ml37
-rw-r--r--tools/coqdep_common.mli2
-rw-r--r--toplevel/coqtop.ml5
15 files changed, 111 insertions, 69 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml
index 8921753814..14c102cede 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -85,6 +85,9 @@ jobs:
coquelicot:
<<: *ci-template
+ cross-crypto:
+ <<: *ci-template
+
elpi:
<<: *ci-template
@@ -160,6 +163,7 @@ workflows:
- compcert: *req-main
- coq-dpdgraph: *req-main
- coquelicot: *req-main
+ - cross-crypto: *req-main
- elpi: *req-main
- equations: *req-main
- geocoq: *req-main
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1789846c83..ac4304da13 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -242,6 +242,9 @@ ci-coq-dpdgraph:
ci-coquelicot:
<<: *ci-template
+ci-cross-crypto:
+ <<: *ci-template
+
ci-elpi:
<<: *ci-template
diff --git a/.travis.yml b/.travis.yml
index eeb0b800e9..d7caf1daf2 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -41,7 +41,7 @@ env:
- COMPILER="system"
- COMPILER_BE="4.06.1"
- CAMLP5_VER=".6.14"
- - CAMLP5_VER_BE=".7.03"
+ - CAMLP5_VER_BE=".7.05"
- FINDLIB_VER=".1.4.1"
- FINDLIB_VER_BE=".1.8.0"
- LABLGTK="lablgtk.2.18.3 lablgtk-extras.1.6"
@@ -76,6 +76,9 @@ matrix:
- TEST_TARGET="ci-coquelicot"
- if: NOT (type = pull_request)
env:
+ - TEST_TARGET="ci-cross-crypto"
+ - if: NOT (type = pull_request)
+ env:
- TEST_TARGET="ci-elpi" EXTRA_OPAM="elpi"
# ppx_tools_versioned requires a specific version findlib
- FINDLIB_VER=""
@@ -278,6 +281,7 @@ install:
- if [ "${TRAVIS_OS_NAME}" == "linux" ]; then travis_retry ./dev/tools/sudo-apt-get-update.sh -q; fi
- if [ "${TRAVIS_OS_NAME}" == "linux" ]; then sudo apt-get install -y opam aspcud gcc-multilib; fi
- opam init -j ${NJOBS} --compiler=${COMPILER} -n -y
+- opam switch "$COMPILER" && opam update
- eval $(opam config env)
- opam config list
- opam install -j ${NJOBS} -y num camlp5${CAMLP5_VER} ocamlfind${FINDLIB_VER} ${EXTRA_OPAM}
diff --git a/Makefile.ci b/Makefile.ci
index 4d4f1df59a..ce725d19dd 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -15,6 +15,7 @@ CI_TARGETS=ci-bignums \
ci-coquelicot \
ci-corn \
ci-cpdt \
+ ci-cross-crypto \
ci-elpi \
ci-equations \
ci-fcsl-pcm \
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 1ae2ad0acb..b7faea13ed 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -91,6 +91,12 @@
: "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}"
########################################################################
+# cross-crypto
+########################################################################
+: "${cross_crypto_CI_BRANCH:=master}"
+: "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto.git}"
+
+########################################################################
# fiat_parsers
########################################################################
: "${fiat_parsers_CI_BRANCH:=master}"
diff --git a/dev/ci/ci-cross-crypto.sh b/dev/ci/ci-cross-crypto.sh
new file mode 100755
index 0000000000..a0d3aa6551
--- /dev/null
+++ b/dev/ci/ci-cross-crypto.sh
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+cross_crypto_CI_DIR="${CI_BUILD_DIR}/cross-crypto"
+
+git_checkout "${cross_crypto_CI_BRANCH}" "${cross_crypto_CI_GITURL}" "${cross_crypto_CI_DIR}"
+( cd "${cross_crypto_CI_DIR}" && git submodule update --init --recursive )
+
+( cd "${cross_crypto_CI_DIR}" && make )
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index d6c340f691..61eb1dafdf 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -8,6 +8,14 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+(* This needs to go trou feedback as it is invoked from IDEs, but
+ ideally we would like to make this independent so it can be
+ bootstrapped. *)
+
+(* Note the problem with the error invokation below calling exit... *)
+(* let error msg = Feedback.msg_error msg *)
+let warning msg = Feedback.msg_warning Pp.(str msg)
+
type arg_source = CmdLine | ProjectFile
type 'a sourced = { thing : 'a; source : arg_source }
@@ -122,7 +130,7 @@ let process_cmd_line orig_dir proj args =
let sourced x = { thing = x; source = if !parsing_project_file then ProjectFile else CmdLine } in
let orig_dir = (* avoids turning foo.v in ./foo.v *)
if orig_dir = "." then "" else orig_dir in
- let error s = Format.eprintf "@[%a]@@\n%!" Pp.pp_with Pp.(str (s^".")); exit 1 in
+ let error s = (Format.eprintf "Error: @[%s@].@\n%!" s; exit 1) in
let mk_path d =
let p = CUnix.correct_path d orig_dir in
{ path = CUnix.remove_path_dot (post_canonize p);
@@ -140,7 +148,7 @@ let process_cmd_line orig_dir proj args =
| ("-full"|"-opt") :: r -> aux { proj with use_ocamlopt = true } r
| "-install" :: d :: r ->
if proj.install_kind <> None then
- Feedback.msg_warning (Pp.str "-install set more than once.");
+ (warning "-install set more than once.@\n%!");
let install = match d with
| "user" -> UserInstall
| "none" -> NoInstall
@@ -167,8 +175,7 @@ let process_cmd_line orig_dir proj args =
let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in
let () = match proj.project_file with
| None -> ()
- | Some _ -> Feedback.msg_warning (Pp.str
- "Multiple project files are deprecated.")
+ | Some _ -> warning "Multiple project files are deprecated.@\n%!"
in
parsing_project_file := true;
let proj = aux { proj with project_file = Some file } (parse file) in
diff --git a/library/lib.ml b/library/lib.ml
index 543cb45bc2..0e41063174 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -183,22 +183,11 @@ let split_lib_gen test =
| before -> after,equal,before
in
let rec findeq after = function
- | hd :: before ->
- if test hd
- then Some (collect after [hd] before)
- else (match hd with
- | (sp,ClosedModule seg)
- | (sp,ClosedSection seg) ->
- (match findeq after seg with
- | None -> findeq (hd::after) before
- | Some (sub_after,sub_equal,sub_before) ->
- Some (sub_after, sub_equal, (List.append sub_before before)))
- | _ -> findeq (hd::after) before)
- | [] -> None
+ | hd :: before when test hd -> collect after [hd] before
+ | hd :: before -> findeq (hd::after) before
+ | [] -> user_err Pp.(str "no such entry")
in
- match findeq [] !lib_state.lib_stk with
- | None -> user_err Pp.(str "no such entry")
- | Some r -> r
+ findeq [] !lib_state.lib_stk
let eq_object_name (fp1, kn1) (fp2, kn2) =
eq_full_path fp1 fp2 && Names.KerName.equal kn1 kn2
diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh
index 11a04d5c2c..6737197ee4 100755
--- a/test-suite/coq-makefile/timing/run.sh
+++ b/test-suite/coq-makefile/timing/run.sh
@@ -44,6 +44,7 @@ TO_SED_IN_BOTH=(
-e s'/ *$//g' # the number of trailing spaces depends on how many digits percentages end up being; since this varies across runs, we remove trailing spaces
-e s'/[0-9]*\.[0-9]*//g' # the precise timing numbers vary, so we strip them out
-e s'/^-*$/------/g' # When none of the numbers get over 100 (or 1000, in per-file), the width of the table is different, so we normalize the number of dashes for table separators
+ -e s'/+/-/g' # some code lines don't really change, but this can show up as either -0m00.01s or +0m00.01s, so we need to normalize the signs; additionally, some N/A's show up where we expect to get -∞ on the per-line file, and so the ∞-replacement gets the sign wrong, so we must correct it
)
TO_SED_IN_PER_FILE=(
@@ -55,7 +56,6 @@ TO_SED_IN_PER_FILE=(
TO_SED_IN_PER_LINE=(
-e s'/0//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start
-e s'/ */ /g' # Sometimes 0 will show up as 0m00.s, sometimes it'll end up being more like 0m00.001s; we must strip out the spaces that result from left-aligning numbers of different widths based on how many digits Coq's [-time] gives
- -e s'/+/-/g' # some code lines don't really change, but this can show up as either -0m00.01s or +0m00.01s, so we need to normalize the signs
)
for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
diff --git a/test-suite/misc/coqc_dash_o.sh b/test-suite/misc/coqc_dash_o.sh
new file mode 100755
index 0000000000..f303214b9a
--- /dev/null
+++ b/test-suite/misc/coqc_dash_o.sh
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+DOUT=misc/tmp_coqc_dash_o/
+OUT=${DOUT}coqc_dash_o.vo
+
+
+mkdir -p "${DOUT}"
+rm -f "${OUT}"
+$coqc misc/coqc_dash_o.v -o "${OUT}"
+if [ ! -f "${OUT}" ]; then
+ printf "coqc -o not working"
+ exit 1
+fi
+rm -fr "${DOUT}"
+exit 0
diff --git a/test-suite/misc/coqc_dash_o.v b/test-suite/misc/coqc_dash_o.v
new file mode 100644
index 0000000000..7426dff1a0
--- /dev/null
+++ b/test-suite/misc/coqc_dash_o.v
@@ -0,0 +1 @@
+Definition x := nat.
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 12b5cab0ac..7db0b28908 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -8,15 +8,24 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Printf
+open Format
open Coqdep_lexer
open Coqdep_common
-open System
+open Minisys
(** The basic parts of coqdep (i.e. the parts used by [coqdep -boot])
are now in [Coqdep_common]. The code that remains here concerns
the other options. Calling this complete coqdep with the [-boot]
option should be equivalent to calling [coqdep_boot].
+
+ As of today, this module depends on the following Coq modules:
+
+ - Flags
+ - Envars
+ - CoqProject_file
+
+ All of it for `coqlib` handling. Ideally we would like to clean
+ coqlib handling up so this can be bootstrapped earlier.
*)
let option_D = ref false
@@ -31,8 +40,7 @@ let warning_mult suf iter =
let d' = Hashtbl.find tab f in
if (Filename.dirname (file_name f d))
<> (Filename.dirname (file_name f d')) then begin
- eprintf "*** Warning : the file %s is defined twice!\n" (f ^ suf);
- flush stderr
+ coqdep_warning "the file %s is defined twice!" (f ^ suf)
end
with Not_found -> () end;
Hashtbl.add tab f d
@@ -80,9 +88,7 @@ let mL_dep_list b f =
while true do
let (Use_module str) = caml_action buf in
if str = b then begin
- eprintf "*** Warning : in file %s the" f;
- eprintf " notation %s. is useless !\n" b;
- flush stderr
+ coqdep_warning "in file %s the notation %s. is useless !\n" f b
end else
if not (List.mem str !deja_vu) then addQueue deja_vu str
done; []
@@ -98,16 +104,13 @@ let affiche_Declare f dcl =
printf "\n*** In file %s: \n" f;
printf "Declare ML Module";
List.iter (fun str -> printf " \"%s\"" str) dcl;
- printf ".\n";
- flush stdout
+ printf ".\n%!"
let warning_Declare f dcl =
- eprintf "*** Warning : in file %s, the ML modules" f;
- eprintf " declaration should be\n";
+ eprintf "*** Warning : in file %s, the ML modules declaration should be\n" f;
eprintf "*** Declare ML Module";
List.iter (fun str -> eprintf " \"%s\"" str) dcl;
- eprintf ".\n";
- flush stderr
+ eprintf ".\n%!"
let traite_Declare f =
let decl_list = ref ([] : string list) in
@@ -149,7 +152,7 @@ let declare_dependencies () =
List.iter
(fun (name,_) ->
traite_Declare (name^".v");
- flush stdout)
+ pp_print_flush std_formatter ())
(List.rev !vAccu)
(** DAGs guaranteed to be transitive reductions *)
@@ -426,11 +429,11 @@ let coq_dependencies_dump chan dumpboxes =
(DAG.empty, List.fold_left (fun ih (file, _) -> insert_raw_graph file ih) [] !vAccu,
List.map fst !vAccu) !vAccu
in
- fprintf chan "digraph dependencies {\n"; flush chan;
+ fprintf chan "digraph dependencies {\n";
if dumpboxes then print_graphs chan (pop_common_prefix graphs)
else List.iter (fun (name, _) -> fprintf chan "\"%s\"[label=\"%s\"]\n" name (basename_noext name)) !vAccu;
DAG.iter (fun name dep -> fprintf chan "\"%s\" -> \"%s\"\n" dep name) deps;
- fprintf chan "}\n"
+ fprintf chan "}\n%!"
end
@@ -498,7 +501,7 @@ let rec parse = function
| "-suffix" :: s :: ll -> suffixe := s ; parse ll
| "-suffix" :: [] -> usage ()
| "-slash" :: ll ->
- Printf.eprintf "warning: option -slash has no effect and is deprecated.\n";
+ coqdep_warning "warning: option -slash has no effect and is deprecated.";
parse ll
| "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
| "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
@@ -509,6 +512,9 @@ let rec parse = function
| f :: ll -> treat_file None f; parse ll
| [] -> ()
+(* Exception to be raised by Envars *)
+exception CoqlibError of string
+
let coqdep () =
if Array.length Sys.argv < 2 then usage ();
if not Coq_config.has_natdynlink then option_dynlink := No;
@@ -520,18 +526,17 @@ let coqdep () =
if !option_boot then begin
add_rec_dir_import add_known "theories" ["Coq"];
add_rec_dir_import add_known "plugins" ["Coq"];
- add_caml_dir "tactics";
add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"];
add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
end else begin
- Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
+ Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg));
let coqlib = Envars.coqlib () in
add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"];
add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"];
let user = coqlib//"user-contrib" in
if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user [];
List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s [])
- (Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (Pp.str x)));
+ (Envars.xdg_dirs ~warn:(fun x -> coqdep_warning "%s" x));
List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath;
end;
List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu;
@@ -547,13 +552,13 @@ let coqdep () =
| None -> ()
| Some (box, file) ->
let chan = open_out file in
- try Graph.coq_dependencies_dump chan box; close_out chan
+ let chan_fmt = formatter_of_out_channel chan in
+ try Graph.coq_dependencies_dump chan_fmt box; close_out chan
with e -> close_out chan; raise e
end
let _ =
try
coqdep ()
- with CErrors.UserError(s,p) ->
- let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p)) in
- Format.eprintf "%a@\n%!" Pp.pp_with pp
+ with CoqlibError msg ->
+ eprintf "*** Error: %s@\n%!" msg
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index db69a3b79d..23b8bc112e 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -8,9 +8,9 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Printf
-open Coqdep_lexer
+open Format
open Unix
+open Coqdep_lexer
open Minisys
(** [coqdep_boot] is a stripped-down version of [coqdep], whose
@@ -20,14 +20,15 @@ open Minisys
options (see for instance [option_dynlink] below).
*)
+let coqdep_warning args =
+ eprintf "*** Warning: @[";
+ kfprintf (fun fmt -> fprintf fmt "@]\n%!") err_formatter args
+
module StrSet = Set.Make(String)
module StrList = struct type t = string list let compare = compare end
module StrListMap = Map.Make(StrList)
-let stderr = Pervasives.stderr
-let stdout = Pervasives.stdout
-
type dynlink = Opt | Byte | Both | No | Variable
let option_c = ref false
@@ -114,8 +115,7 @@ let same_path_opt s s' =
let warning_ml_clash x s suff s' suff' =
if suff = suff' && not (same_path_opt s s') then
- eprintf
- "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff
+ coqdep_warning "%s%s already found in %s (discarding %s%s)\n" x suff
(match s with None -> "." | Some d -> d)
((match s' with None -> "." | Some d -> d) // x) suff
@@ -180,13 +180,11 @@ let error_cannot_parse s (i,j) =
exit 1
let warning_module_notfound f s =
- eprintf "*** Warning: in file %s, library %s is required and has not been found in the loadpath!\n%!"
+ coqdep_warning "in file %s, library %s is required and has not been found in the loadpath!"
f (String.concat "." s)
let warning_declare f s =
- eprintf "*** Warning: in file %s, declared ML module " f;
- eprintf "%s has not been found!\n" s;
- flush stderr
+ coqdep_warning "in file %s, declared ML module %s has not been found!" f s
let warning_clash file dir =
match StrListMap.find dir !clash_v with
@@ -203,8 +201,7 @@ let warning_clash file dir =
| _ -> assert false
let warning_cannot_open_dir dir =
- eprintf "*** Warning: cannot open %s\n" dir;
- flush stderr
+ coqdep_warning "cannot open %s" dir
let safe_assoc from verbose file k =
if verbose && StrListMap.mem k !clash_v then warning_clash file k;
@@ -451,15 +448,13 @@ let mL_dependencies () =
in
let efullname = escape fullname in
printf "%s.cmo:%s%s\n" efullname dep intf;
- printf "%s.cmx:%s%s\n" efullname dep_opt intf;
- flush stdout)
+ printf "%s.cmx:%s%s\n%!" efullname dep_opt intf)
(List.rev !mlAccu);
List.iter
(fun (name,dirname) ->
let fullname = file_name name dirname in
let (dep,_) = traite_fichier_ML fullname ".mli" in
- printf "%s.cmi:%s\n" (escape fullname) dep;
- flush stdout)
+ printf "%s.cmi:%s\n%!" (escape fullname) dep)
(List.rev !mliAccu);
List.iter
(fun (name,dirname) ->
@@ -468,8 +463,7 @@ let mL_dependencies () =
let efullname = escape fullname in
printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname (String.concat " " dep);
printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
- printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
- flush stdout)
+ printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n%!" efullname efullname)
(List.rev !mllibAccu);
List.iter
(fun (name,dirname) ->
@@ -483,7 +477,7 @@ let mL_dependencies () =
List.iter (fun dep ->
printf "%s.cmx : FOR_PACK=-for-pack %s\n" dep efullname_capital)
dep;
- flush stdout)
+ printf "%!")
(List.rev !mlpackAccu)
let coq_dependencies () =
@@ -496,8 +490,7 @@ let coq_dependencies () =
printf "\n";
printf "%s.vio: %s.v" ename ename;
traite_fichier_Coq ".vio" true (name ^ ".v");
- printf "\n";
- flush stdout)
+ printf "\n%!")
(List.rev !vAccu)
let rec suffixes = function
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index d0d7932435..91d2b45876 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -10,6 +10,8 @@
module StrSet : Set.S with type elt = string
+val coqdep_warning : ('a, Format.formatter, unit, unit) format4 -> 'a
+
(** [find_dir_logpath dir] Return the logical path of directory [dir]
if it has been given one. Raise [Not_found] otherwise. In
particular we can check if "." has been attributed a logical path
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 38351a377a..809490166c 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -315,11 +315,12 @@ let compile cur_feeder opts ~echo ~f_in ~f_out =
CoqworkmgrApi.giveback 1
let compile_file cur_feeder opts (f_in, echo) =
+ let f_out = opts.compilation_output_name in
if !Flags.beautify then
Flags.with_option Flags.beautify_file
- (fun f_in -> compile cur_feeder opts ~echo ~f_in ~f_out:None) f_in
+ (fun f_in -> compile cur_feeder opts ~echo ~f_in ~f_out) f_in
else
- compile cur_feeder opts ~echo ~f_in ~f_out:None
+ compile cur_feeder opts ~echo ~f_in ~f_out
let compile_files cur_feeder opts =
let compile_list = List.rev opts.compile_list in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 16:28:46 +0000