diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 10 | ||||
| -rwxr-xr-x | tools/beautify-archive | 2 | ||||
| -rwxr-xr-x | tools/check-translate | 2 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 6 | ||||
| -rw-r--r-- | tools/coqc.ml | 2 | ||||
| -rw-r--r-- | tools/coqdoc/index.ml | 2 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 34 |
7 files changed, 29 insertions, 29 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index e54ea45d41..9f891afe53 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -63,11 +63,11 @@ VERBOSE ?= # Time the Coq process (set to non empty), and how (see default value) TIMED?= TIMECMD?= -# Use /usr/bin/time on linux, gtime on Mac OS +# Use /usr/bin/env time on linux, gtime on Mac OS TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)" ifneq (,$(TIMED)) -ifeq (0,$(shell /usr/bin/time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) -STDTIME?=/usr/bin/time -f $(TIMEFMT) +ifeq (0,$(shell /usr/bin/env time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=/usr/bin/env time -f $(TIMEFMT) else ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) STDTIME?=gtime -f $(TIMEFMT) @@ -76,7 +76,7 @@ STDTIME?=time endif endif else -STDTIME?=/usr/bin/time -f $(TIMEFMT) +STDTIME?=/usr/bin/env time -f $(TIMEFMT) endif # Coq binaries @@ -170,7 +170,7 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") -CAMLFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) +CAMLFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) $(OCAML_API_FLAGS) CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib) diff --git a/tools/beautify-archive b/tools/beautify-archive index 6bfa974a53..a327ea44e1 100755 --- a/tools/beautify-archive +++ b/tools/beautify-archive @@ -23,7 +23,7 @@ cp -pr /tmp/$OLDARCHIVE.$$ $NEWARCHIVE cd $NEWARCHIVE rm description || true make clean -make COQFLAGS='-beautify -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \ +make COQFLAGS='-beautify -q $(OPT) $(COQLIBS) $(OTHERFLAGS)' || \ { echo ---- Failed to beautify; exit 1; } echo -------- Upgrading files in the beautification directory -------------- beaufiles=`find . -name \*.v$BEAUTIFYSUFFIX` diff --git a/tools/check-translate b/tools/check-translate index 3dd8240532..acb6f45903 100755 --- a/tools/check-translate +++ b/tools/check-translate @@ -2,7 +2,7 @@ echo -------------- Producing translated files --------------------- rm */*/*.v8 >& /dev/null -make COQ_XML=-translate theories || { echo ---- Failed to translate; exit 1; } +make COQOPTS=-translate theories || { echo ---- Failed to translate; exit 1; } if [ -e translated ]; then rm -r translated; fi if [ -e successful-translation ]; then rm -r successful-translation; fi if [ -e failed-translation ]; then rm -r failed-translation; fi diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 327f53520c..0f38d19386 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -203,8 +203,12 @@ let generate_conf_coq_config oc args bypass_API = section oc "Coq configuration."; let src_dirs = if bypass_API then Coq_config.all_src_dirs - else Coq_config.api_dirs @ Coq_config.plugins_dirs @ ["-open API"] in + else Coq_config.api_dirs @ Coq_config.plugins_dirs in Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs; + if bypass_API then + Printf.fprintf oc "OCAML_API_FLAGS=\n" + else + Printf.fprintf oc "OCAML_API_FLAGS=-open API\n"; fprintf oc "COQMF_WINDRIVE=%s\n" (windrive Coq_config.coqlib) ;; diff --git a/tools/coqc.ml b/tools/coqc.ml index 4595af6e88..862225d3d1 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -94,7 +94,7 @@ let parse_args () = | ("-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac" |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob" |"-q"|"-profile"|"-just-parsing"|"-echo" |"-quiet" - |"-silent"|"-m"|"-xml"|"-beautify"|"-strict-implicit" + |"-silent"|"-m"|"-beautify"|"-strict-implicit" |"-impredicative-set"|"-vm"|"-native-compiler" |"-indices-matter"|"-quick"|"-type-in-type" |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch" diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index 8ba6156709..1bbf76490d 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -117,7 +117,7 @@ let find_module m = if Hashtbl.mem local_modules m then Local else - try External (Filename.concat (find_external_library m) m) + try External (find_external_library m ^ "/" ^ m) with Not_found -> Unknown diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 5c0d2a39b0..d043c4a584 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -693,25 +693,21 @@ module Html = struct printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s) let ident s loc = - if is_keyword s then begin - printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s) - end else begin - try - match loc with - | None -> raise Not_found - | Some loc -> - reference (translate s) (Index.find (get_module false) loc) - with Not_found -> - if is_tactic s then - printf "<span class=\"id\" title=\"tactic\">%s</span>" (translate s) - else - if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) - then - try reference (translate s) (Index.find_string (get_module false) s) - with _ -> Tokens.output_tagged_ident_string s - else - Tokens.output_tagged_ident_string s - end + try + match loc with + | None -> raise Not_found + | Some loc -> + reference (translate s) (Index.find (get_module false) loc) + with Not_found -> + if is_tactic s then + printf "<span class=\"id\" title=\"tactic\">%s</span>" (translate s) + else if is_keyword s then + printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s) + else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then + try reference (translate s) (Index.find_string (get_module false) s) + with Not_found -> Tokens.output_tagged_ident_string s + else + Tokens.output_tagged_ident_string s let proofbox () = printf "<font size=-2>☐</font>" |