diff options
| -rw-r--r-- | .circleci/config.yml | 6 | ||||
| -rw-r--r-- | .github/CODEOWNERS | 12 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 121 | ||||
| -rw-r--r-- | .travis.yml | 6 | ||||
| -rw-r--r-- | Makefile.ci | 1 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 6 | ||||
| -rwxr-xr-x | dev/ci/ci-cross-crypto.sh | 11 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 2 | ||||
| -rwxr-xr-x | dev/ci/docker/bionic_coq/hooks/post_push | 2 | ||||
| -rw-r--r-- | lib/control.ml | 5 | ||||
| -rw-r--r-- | lib/control.mli | 5 | ||||
| -rw-r--r-- | lib/coqProject_file.ml4 | 15 | ||||
| -rw-r--r-- | tools/coqdep.ml | 53 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 37 | ||||
| -rw-r--r-- | tools/coqdep_common.mli | 2 |
15 files changed, 183 insertions, 101 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index c4b7733a65..14c102cede 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -8,7 +8,7 @@ defaults: # reference syntax) working_directory: ~/coq docker: - - image: coqci/base:V2018-05-07 + - image: coqci/base:V2018-05-07-V2 environment: &envvars NATIVE_COMP: "yes" @@ -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/.github/CODEOWNERS b/.github/CODEOWNERS index afa95420ca..ab9725c967 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -71,9 +71,9 @@ /engine/ @ppedrot # Secondary maintainer @aspiwack -/engine/universes.ml{,i} @SkySkimmer -/engine/univops.ml{,i} @SkySkimmer -/engine/uState.ml{,i} @SkySkimmer +/engine/universes.* @SkySkimmer +/engine/univops.* @SkySkimmer +/engine/uState.* @SkySkimmer # Secondary maintainer @mattam82 ########## Grammar macros ########## @@ -99,9 +99,9 @@ /kernel/byterun/ @maximedenes # Secondary maintainer @silene -/kernel/sorts.ml{,i} @SkySkimmer -/kernel/uGraph.ml{,i} @SkySkimmer -/kernel/univ.ml{,i} @SkySkimmer +/kernel/sorts.* @SkySkimmer +/kernel/uGraph.* @SkySkimmer +/kernel/univ.* @SkySkimmer # Secondary maintainer @mattam82 ########## Library ########## diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 78850fa5ee..ac4304da13 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -1,4 +1,4 @@ -image: coqci/base:V2018-05-07 +image: coqci/base:V2018-05-07-V2 stages: - build @@ -8,7 +8,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: bionic_coq-V2018-05-03 + CACHEKEY: bionic_coq-V2018-05-07-V2 # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" # Used to select special compiler switches such as flambda, 32bits, etc... @@ -19,7 +19,7 @@ before_script: - ls -a # figure out if artifacts are around - printenv | sort - declare -A switch_table - - switch_table=( ["base"]="$COMPILER" ["be"]="$COMPILER_BE" ) + - switch_table=( ["base"]="$COMPILER" ["edge"]="$COMPILER_BE" ) - opam switch -y "${switch_table[$OPAM_SWITCH]}$OPAM_VARIANT" - eval $(opam config env) - opam list @@ -43,7 +43,7 @@ before_script: - set -e - echo 'start:coq.config' - - ./configure -prefix "$(pwd)/_install_ci" ${EXTRA_CONF} + - ./configure -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE" - echo 'end:coq.config' - echo 'start:coq.build' @@ -67,7 +67,7 @@ before_script: - set -e - echo 'start:coq.config' - - ./configure -local ${EXTRA_CONF} + - ./configure -local ${COQ_EXTRA_CONF} - echo 'end:coq.config' - echo 'start:coq.build' @@ -76,7 +76,7 @@ before_script: - set +e variables: &warnings-variables - EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only" + COQ_EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only" # every non build job must set dependencies otherwise all build # artifacts are used together and we may get some random Coq. To that @@ -121,29 +121,46 @@ before_script: - echo 'end:coq.test' - set +e dependencies: - - build + - build:base variables: &ci-template-vars TEST_TARGET: "$CI_JOB_NAME" -build: +.ci-template-flambda: &ci-template-flambda + <<: *ci-template + dependencies: + - build:edge+flambda + variables: + <<: *ci-template-vars + OPAM_SWITCH: "edge" + OPAM_VARIANT: "+flambda" + +build:base: <<: *build-template variables: - EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes" + COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes" # no coqide for 32bit: libgtk installation problems -build:32bit: +build:base+32bit: <<: *build-template variables: OPAM_VARIANT: "+32bit" - EXTRA_CONF: "-native-compiler yes" + COQ_EXTRA_CONF: "-native-compiler yes" -build:bleeding-edge: +build:edge: <<: *build-template variables: - OPAM_SWITCH: be - EXTRA_CONF: "-native-compiler yes -coqide opt" + OPAM_SWITCH: edge + COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" -warnings: +build:edge+flambda: + <<: *build-template + variables: + OPAM_SWITCH: edge + OPAM_VARIANT: "+flambda" + COQ_EXTRA_CONF: "-native-compiler no -coqide opt -flambda-opts " + COQ_EXTRA_CONF_QUOTE: "-O3 -unbox-closures" + +warnings:base: <<: *warnings-template # warnings:32bit: @@ -151,50 +168,73 @@ warnings: # variables: # <<: *warnings-variables -warnings:bleeding-edge: +warnings:edge: <<: *warnings-template variables: - OPAM_SWITCH: be + OPAM_SWITCH: edge -test-suite: +test-suite:base: <<: *test-suite-template dependencies: - - build + - build:base -test-suite:32bit: +test-suite:base+32bit: <<: *test-suite-template dependencies: - - build:32bit + - build:base+32bit variables: OPAM_VARIANT: "+32bit" -test-suite:bleeding-edge: +test-suite:edge: <<: *test-suite-template dependencies: - - build:bleeding-edge + - build:edge variables: - OPAM_SWITCH: be + OPAM_SWITCH: edge -validate: +test-suite:edge+flambda: + <<: *test-suite-template + dependencies: + - build:edge+flambda + variables: + OPAM_SWITCH: edge + OPAM_VARIANT: "+flambda" + +validate:base: <<: *validate-template dependencies: - - build + - build:base -validate:32bit: +validate:base+32bit: <<: *validate-template dependencies: - - build:32bit + - build:base+32bit variables: OPAM_VARIANT: "+32bit" +validate:edge: + <<: *validate-template + dependencies: + - build:edge + variables: + OPAM_SWITCH: edge + +validate:edge+flambda: + <<: *validate-template + dependencies: + - build:edge+flambda + variables: + OPAM_SWITCH: edge + OPAM_VARIANT: "+flambda" + ci-bignums: <<: *ci-template ci-color: - <<: *ci-template + <<: *ci-template-flambda ci-compcert: - <<: *ci-template + <<: *ci-template-flambda ci-coq-dpdgraph: <<: *ci-template @@ -202,6 +242,9 @@ ci-coq-dpdgraph: ci-coquelicot: <<: *ci-template +ci-cross-crypto: + <<: *ci-template + ci-elpi: <<: *ci-template @@ -211,10 +254,8 @@ ci-equations: ci-fcsl-pcm: <<: *ci-template -# ci-fiat-crypto: -# <<: *ci-template -# # out of memory error -# allow_failure: true +ci-fiat-crypto: + <<: *ci-template-flambda ci-fiat-parsers: <<: *ci-template @@ -223,16 +264,16 @@ ci-flocq: <<: *ci-template ci-formal-topology: - <<: *ci-template + <<: *ci-template-flambda ci-geocoq: - <<: *ci-template + <<: *ci-template-flambda ci-hott: <<: *ci-template ci-iris-lambda-rust: - <<: *ci-template + <<: *ci-template-flambda ci-ltac2: <<: *ci-template @@ -241,7 +282,7 @@ ci-math-classes: <<: *ci-template ci-math-comp: - <<: *ci-template + <<: *ci-template-flambda ci-mtac2: <<: *ci-template @@ -253,7 +294,7 @@ ci-sf: <<: *ci-template ci-unimath: - <<: *ci-template + <<: *ci-template-flambda ci-vst: - <<: *ci-template + <<: *ci-template-flambda 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/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 9201001574..689d203a16 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -43,4 +43,4 @@ RUN opam switch -y -j $NJOBS $COMPILER_BE && eval $(opam config env) && \ # BE+flambda switch RUN opam switch -y -j $NJOBS "${COMPILER_BE}+flambda" && eval $(opam config env) && \ - opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE + opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE $CI_OPAM diff --git a/dev/ci/docker/bionic_coq/hooks/post_push b/dev/ci/docker/bionic_coq/hooks/post_push index 6daf337a72..307680aa51 100755 --- a/dev/ci/docker/bionic_coq/hooks/post_push +++ b/dev/ci/docker/bionic_coq/hooks/post_push @@ -1,6 +1,6 @@ #!/usr/bin/env bash -COQCI_VERSION=V2018-05-07 +COQCI_VERSION=V2018-05-07-V2 docker tag $IMAGE_NAME $DOCKER_REPO:$COQCI_VERSION docker push $DOCKER_REPO:$COQCI_VERSION diff --git a/lib/control.ml b/lib/control.ml index e67cd8b38d..3fbeb168c4 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -85,4 +85,7 @@ let timeout_fun = match Sys.os_type with | "Unix" | "Cygwin" -> { timeout = unix_timeout } | _ -> { timeout = windows_timeout } -let timeout n f e = timeout_fun.timeout n f e +let timeout_fun_ref = ref timeout_fun +let set_timeout f = timeout_fun_ref := f + +let timeout n f e = !timeout_fun_ref.timeout n f e diff --git a/lib/control.mli b/lib/control.mli index 415e054625..59e2a15158 100644 --- a/lib/control.mli +++ b/lib/control.mli @@ -24,3 +24,8 @@ val check_for_interrupt : unit -> unit val timeout : int -> ('a -> 'b) -> 'a -> exn -> 'b (** [timeout n f x e] tries to compute [f x], and if it fails to do so before [n] seconds, it raises [e] instead. *) + +(** Set a particular timeout function; warning, this is an internal + API and it is scheduled to go away. *) +type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b } +val set_timeout : timeout -> unit 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/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 |