aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in81
-rw-r--r--tools/TimeFileMaker.py4
-rwxr-xr-xtools/beautify-archive2
-rwxr-xr-xtools/check-translate2
-rw-r--r--tools/coq_makefile.ml21
-rw-r--r--tools/coqc.ml11
-rw-r--r--tools/coqdep_lexer.mll42
-rw-r--r--tools/coqdoc/cpretty.mll19
-rw-r--r--tools/coqdoc/index.ml2
-rw-r--r--tools/coqdoc/output.ml34
-rw-r--r--tools/coqmktop.ml22
-rw-r--r--tools/coqwc.mll2
-rw-r--r--tools/fake_ide.ml6
13 files changed, 141 insertions, 107 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index f1e519d038..8f79f8a669 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -39,6 +39,7 @@ CAMLP4O := $(COQMF_CAMLP4O)
CAMLP4BIN := $(COQMF_CAMLP4BIN)
CAMLP4LIB := $(COQMF_CAMLP4LIB)
CAMLP4OPTIONS := $(COQMF_CAMLP4OPTIONS)
+CAMLFLAGS := $(COQMF_CAMLFLAGS)
HASNATDYNLINK := $(COQMF_HASNATDYNLINK)
@CONF_FILE@: @PROJECT_FILE@
@@ -52,7 +53,7 @@ HASNATDYNLINK := $(COQMF_HASNATDYNLINK)
#
# Parameters are make variable assignments.
# They can be passed to (each call to) make on the command line.
-# They can also be put in @LOCAL_FILE@ once an forall.
+# They can also be put in @LOCAL_FILE@ once an for all.
# For retro-compatibility reasons they can be put in the _CoqProject, but this
# practice is discouraged since _CoqProject better not contain make specific
# code (be nice to user interfaces).
@@ -63,11 +64,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 +77,7 @@ STDTIME?=time
endif
endif
else
-STDTIME?=/usr/bin/time -f $(TIMEFMT)
+STDTIME?=/usr/bin/env time -f $(TIMEFMT)
endif
# Coq binaries
@@ -96,12 +97,15 @@ COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-fil
BEFORE ?=
AFTER ?=
+# FIXME this should be generated by Coq (modules already linked by Coq)
+CAMLDONTLINK=camlp5.gramlib,unix,str
+
# OCaml binaries
-CAMLC ?= "$(OCAMLFIND)" ocamlc -c -rectypes -thread
-CAMLOPTC ?= "$(OCAMLFIND)" opt -c -rectypes -thread
-CAMLLINK ?= "$(OCAMLFIND)" ocamlc -rectypes -thread
-CAMLOPTLINK ?= "$(OCAMLFIND)" opt -rectypes -thread
-CAMLDOC ?= "$(OCAMLFIND)" ocamldoc -rectypes
+CAMLC ?= "$(OCAMLFIND)" ocamlc -c
+CAMLOPTC ?= "$(OCAMLFIND)" opt -c
+CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkpkg -dontlink $(CAMLDONTLINK)
+CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkpkg -dontlink $(CAMLDONTLINK)
+CAMLDOC ?= "$(OCAMLFIND)" ocamldoc
CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack
# DESTDIR is prepended to all installation paths
@@ -111,6 +115,9 @@ DESTDIR ?=
CAMLDEBUG ?=
COQDEBUG ?=
+# Extra packages to be linked in (as in findlib -package)
+CAMLPKGS ?=
+
# Option for making timing files
TIMING?=
# Output file names for timed builds
@@ -151,7 +158,7 @@ OPT?=
# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d
ifeq '$(OPT)' '-byte'
USEBYTE:=true
-DYNOBJ:=.cmo
+DYNOBJ:=.cma
DYNLIB:=.cma
else
USEBYTE:=
@@ -170,9 +177,7 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@
COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)")
-CAMLFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)
-
-CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib)
+CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) $(OCAML_API_FLAGS)
# FIXME This should be generated by Coq
GRAMMARS:=grammar.cma
@@ -182,7 +187,12 @@ else
CAMLP4EXTEND=
endif
-PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" compat5.cmo $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'
+CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null)
+ifeq (,$(CAMLLIB))
+PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.")
+else
+PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'
+endif
ifneq (,$(TIMING))
TIMING_ARG=-time
@@ -199,8 +209,8 @@ else
TIMING_ARG=
endif
-# Retro compatibility (DESTDIR is standard on Unix, DESTROOT is not)
-ifneq "$(DSTROOT)" ""
+# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not)
+ifdef DSTROOT
DESTDIR := $(DSTROOT)
endif
@@ -440,7 +450,7 @@ beautify: $(BEAUTYFILES)
# There rules can be extended in @LOCAL_FILE@
# Extensions can't assume when they run.
-install: install-extra
+install:
$(HIDE)for f in $(FILESTOINSTALL); do\
df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
if [ "$$?" != "0" -o -z "$$df" ]; then\
@@ -451,6 +461,7 @@ install: install-extra
echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
fi;\
done
+ $(HIDE)$(MAKE) install-extra -f "$(SELF)"
install-extra::
@# Extension point
.PHONY: install install-extra
@@ -491,7 +502,7 @@ uninstall::
instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
rm -f "$$instf" &&\
echo RM "$$instf" &&\
- (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" || true); \
+ (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \
done
.PHONY: uninstall
@@ -558,46 +569,51 @@ archclean::
$(MLIFILES:.mli=.cmi): %.cmi: %.mli
$(SHOW)'CAMLC -c $<'
- $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $<
+ $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4
$(SHOW)'CAMLC -pp -c $<'
- $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(PP) -impl $<
+ $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) -impl $<
$(ML4FILES:.ml4=.cmx): %.cmx: %.ml4
$(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<'
- $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(PP) $(FOR_PACK) -impl $<
+ $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) $(FOR_PACK) -impl $<
$(MLFILES:.ml=.cmo): %.cmo: %.ml
$(SHOW)'CAMLC -c $<'
- $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $<
+ $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
$(MLFILES:.ml=.cmx): %.cmx: %.ml
$(SHOW)'CAMLOPT -c $(FOR_PACK) $<'
- $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(FOR_PACK) $<
+ $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $<
$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa
$(SHOW)'CAMLOPT -shared -o $@'
- $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) \
+ $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
-linkall -shared -o $@ $<
$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib
$(SHOW)'CAMLC -a -o $@'
- $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^
+ $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib
$(SHOW)'CAMLOPT -a -o $@'
- $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^
+ $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
-$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmx
+$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa
$(SHOW)'CAMLOPT -shared -o $@'
- $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $<
+ $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+ -shared -linkall -o $@ $<
+
+$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx
+ $(SHOW)'CAMLOPT -a -o $@'
+ $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $<
$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack
$(SHOW)'CAMLC -a -o $@'
- $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^
+ $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack
$(SHOW)'CAMLC -pack -o $@'
@@ -610,7 +626,8 @@ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
# This rule is for _CoqProject with no .mllib nor .mlpack
$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx
$(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
- $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $<
+ $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+ -shared -o $@ $<
ifneq (,$(TIMING))
TIMING_EXTRA = > $<.$(TIMING_EXT)
@@ -734,7 +751,7 @@ printenv::
# file you can extend the merlin-hook target in @LOCAL_FILE@
.merlin:
$(SHOW)'FILL .merlin'
- $(HIDE)echo 'FLG -rectypes' > .merlin
+ $(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin
$(HIDE)echo 'B $(COQLIB)' >> .merlin
$(HIDE)echo 'S $(COQLIB)' >> .merlin
$(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \
diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py
index a207c2171b..7298ef5e8e 100644
--- a/tools/TimeFileMaker.py
+++ b/tools/TimeFileMaker.py
@@ -28,10 +28,10 @@ def get_times(file_name):
else:
with open(file_name, 'r') as f:
lines = f.read()
- reg = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)$', re.MULTILINE)
+ reg = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE)
times = reg.findall(lines)
if all(time in ('0.00', '0.01') for name, time in times):
- reg = re.compile(r'^([^\s]*) \([^\)]*?real: ([0-9\.]+)[^\)]*?\)$', re.MULTILINE)
+ reg = re.compile(r'^([^\s]*) \([^\)]*?real: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE)
times = reg.findall(lines)
if all(STRIP_REG.search(name.strip()) for name, time in times):
times = tuple((STRIP_REG.sub(STRIP_REP, name.strip()), time) for name, time in times)
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..2feaaa04cd 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -114,16 +114,16 @@ let read_whole_file s =
close_in ic;
Buffer.contents b
-let makefile_template =
- let template = "/tools/CoqMakefile.in" in
- Coq_config.coqlib ^ template
-
let quote s = if String.contains s ' ' then "'" ^ s ^ "'" else s
let generate_makefile oc conf_file local_file args project =
+ let makefile_template =
+ let template = "/tools/CoqMakefile.in" in
+ Envars.coqlib () ^ template in
let s = read_whole_file makefile_template in
let s = List.fold_left
- (fun s (k,v) -> Str.global_replace (Str.regexp_string k) v s) s
+ (* We use global_substitute to avoid running into backslash issues due to \1 etc. *)
+ (fun s (k,v) -> Str.global_substitute (Str.regexp_string k) (fun _ -> v) s) s
[ "@CONF_FILE@", conf_file;
"@LOCAL_FILE@", local_file;
"@COQ_VERSION@", Coq_config.version;
@@ -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)
;;
@@ -271,7 +275,7 @@ let generate_conf oc project args =
;;
let ensure_root_dir
- ({ ml_includes; r_includes;
+ ({ ml_includes; r_includes; q_includes;
v_files; ml_files; mli_files; ml4_files;
mllib_files; mlpack_files } as project)
=
@@ -280,6 +284,7 @@ let ensure_root_dir
let not_tops = List.for_all (fun s -> s <> Filename.basename s) in
if exists (fun { canonical_path = x } -> x = here) ml_includes
|| exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes
+ || exists (fun ({ canonical_path = x },_) -> is_prefix x here) q_includes
|| (not_tops v_files &&
not_tops mli_files && not_tops ml4_files && not_tops ml_files &&
not_tops mllib_files && not_tops mlpack_files)
@@ -420,7 +425,7 @@ let _ =
check_overlapping_include project;
- Envars.set_coqlib ~fail:(fun x -> x);
+ Envars.set_coqlib ~fail:(fun x -> Printf.eprintf "Error: %s\n" x; exit 1);
let ocm = Option.cata open_out stdout project.makefile in
generate_makefile ocm conf_file local_file (prog :: args) project;
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 5da203742c..b381c5ba42 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -86,16 +86,15 @@ let parse_args () =
Envars.print_config stdout Coq_config.all_src_dirs;
exit 0
- |"--print-version" :: _ ->
+ | ("-print-version" | "--print-version") :: _ ->
Usage.machine_readable_version 0
(* Options for coqtop : a) options with 0 argument *)
- | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac"
+ | ("-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac"
|"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob"
- |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
- |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
- |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
+ |"-q"|"-profile"|"-echo" |"-quiet"
+ |"-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"
@@ -110,7 +109,7 @@ let parse_args () =
|"-load-ml-source"|"-require"|"-load-ml-object"
|"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"
|"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w"
- |"-o"|"-profile-ltac-cutoff"
+ |"-o"|"-profile-ltac-cutoff"
as o) :: rem ->
begin
match rem with
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 8eeb59898f..564e20d0e8 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -25,8 +25,6 @@
exception Fin_fichier
exception Syntax_error of int*int
- let field_name s = String.sub s 1 (String.length s - 1)
-
let unquote_string s =
String.sub s 1 (String.length s - 2)
@@ -40,6 +38,18 @@
let syntax_error lexbuf =
raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf))
+ let check_valid lexbuf s =
+ match Unicode.ident_refutation s with
+ | None -> s
+ | Some _ -> syntax_error lexbuf
+
+ let get_ident lexbuf =
+ let s = Lexing.lexeme lexbuf in check_valid lexbuf s
+
+ let get_field_name lexbuf =
+ let s = Lexing.lexeme lexbuf in
+ check_valid lexbuf (String.sub s 1 (String.length s - 1))
+
[@@@ocaml.warning "-3"] (* String.uncapitalize_ascii since 4.03.0 GPR#124 *)
let uncapitalize = String.uncapitalize
[@@@ocaml.warning "+3"]
@@ -52,20 +62,8 @@ let identchar = ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9']
let caml_up_ident = uppercase identchar*
let caml_low_ident = lowercase identchar*
-let coq_firstchar =
- (* This is only an approximation, refer to lib/util.ml for correct def *)
- ['A'-'Z' 'a'-'z' '_'] |
- (* superscript 1 *)
- '\194' '\185' |
- (* utf-8 latin 1 supplement *)
- '\195' ['\128'-'\150'] | '\195' ['\152'-'\182'] | '\195' ['\184'-'\191'] |
- (* utf-8 letters *)
- '\206' (['\145'-'\161'] | ['\163'-'\187'])
- '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
- | '\129' [ '\176'-'\187' ] (* superscripts *)
- | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
-let coq_identchar = coq_firstchar | ['\'' '0'-'9']
-let coq_ident = coq_firstchar coq_identchar*
+(* This is an overapproximation, we check correctness afterwards *)
+let coq_ident = ['A'-'Z' 'a'-'z' '_' '\128'-'\255'] ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9' '\128'-'\255']*
let coq_field = '.' coq_ident
let dot = '.' ( space+ | eof)
@@ -102,7 +100,7 @@ and from_rule = parse
| space+
{ from_rule lexbuf }
| coq_ident
- { let from = coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf in
+ { let from = coq_qual_id_tail [get_ident lexbuf] lexbuf in
consume_require (Some from) lexbuf }
| eof
{ syntax_error lexbuf }
@@ -241,7 +239,7 @@ and load_file = parse
parse_dot lexbuf;
Load (unquote_vfile_string s) }
| coq_ident
- { let s = lexeme lexbuf in skip_to_dot lexbuf; Load s }
+ { let s = get_ident lexbuf in skip_to_dot lexbuf; Load s }
| eof
{ syntax_error lexbuf }
| _
@@ -253,7 +251,7 @@ and require_file from = parse
| space+
{ require_file from lexbuf }
| coq_ident
- { let name = coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf in
+ { let name = coq_qual_id_tail [get_ident lexbuf] lexbuf in
let qid = coq_qual_id_list [name] lexbuf in
parse_dot lexbuf;
Require (from, qid) }
@@ -278,7 +276,7 @@ and coq_qual_id = parse
| space+
{ coq_qual_id lexbuf }
| coq_ident
- { coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf }
+ { coq_qual_id_tail [get_ident lexbuf] lexbuf }
| _
{ syntax_error lexbuf }
@@ -288,7 +286,7 @@ and coq_qual_id_tail module_name = parse
| space+
{ coq_qual_id_tail module_name lexbuf }
| coq_field
- { coq_qual_id_tail (field_name (Lexing.lexeme lexbuf) :: module_name) lexbuf }
+ { coq_qual_id_tail (get_field_name lexbuf :: module_name) lexbuf }
| eof
{ syntax_error lexbuf }
| _
@@ -301,7 +299,7 @@ and coq_qual_id_list module_names = parse
| space+
{ coq_qual_id_list module_names lexbuf }
| coq_ident
- { let name = coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf in
+ { let name = coq_qual_id_tail [get_ident lexbuf] lexbuf in
coq_qual_id_list (name :: module_names) lexbuf
}
| eof
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 60a245dc4d..186f6cf6cf 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -682,7 +682,7 @@ and doc_bol = parse
| space* nl+
{ Output.paragraph (); doc_bol lexbuf }
| "<<" space*
- { Output.start_verbatim false; verbatim false lexbuf; doc_bol lexbuf }
+ { Output.start_verbatim false; verbatim 0 false lexbuf; doc_bol lexbuf }
| eof
{ true }
| '_'
@@ -707,7 +707,7 @@ and doc_list_bol indents = parse
}
| "<<" space*
{ Output.start_verbatim false;
- verbatim false lexbuf;
+ verbatim 0 false lexbuf;
doc_list_bol indents lexbuf }
| "[[" nl
{ formatted := true;
@@ -852,7 +852,7 @@ and doc indents = parse
Output.char (lexeme_char lexbuf 1);
doc indents lexbuf }
| "<<" space*
- { Output.start_verbatim true; verbatim true lexbuf; doc_bol lexbuf }
+ { Output.start_verbatim true; verbatim 0 true lexbuf; doc_bol lexbuf }
| '"'
{ if !Cdglobals.plain_comments
then Output.char '"'
@@ -892,13 +892,20 @@ and escaped_html = parse
{ backtrack lexbuf }
| _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
-and verbatim inline = parse
+and verbatim depth inline = parse
| nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
| nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
| ">>" { Output.stop_verbatim inline }
- | "*)" { Output.stop_verbatim inline; backtrack lexbuf }
+ | "(*" { Output.verbatim_char inline '(';
+ Output.verbatim_char inline '*';
+ verbatim (depth+1) inline lexbuf }
+ | "*)" { if (depth == 0)
+ then (Output.stop_verbatim inline; backtrack lexbuf)
+ else (Output.verbatim_char inline '*';
+ Output.verbatim_char inline ')';
+ verbatim (depth-1) inline lexbuf) }
| eof { Output.stop_verbatim inline }
- | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim inline lexbuf }
+ | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim depth inline lexbuf }
and url = parse
| "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer }
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>&#9744;</font>"
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index 30e098df59..950ed53ccf 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -32,6 +32,8 @@ let supported_suffix f = match CUnix.get_extension f with
| ".ml" | ".cmx" | ".cmo" | ".cmxa" | ".cma" | ".c" -> true
| _ -> false
+let supported_flambda_option f = List.mem f Coq_config.flambda_flags
+
(** From bytecode extension to native
*)
let native_suffix f = match CUnix.get_extension f with
@@ -175,8 +177,6 @@ let parse_args () =
| "-top" :: rem -> top := true ; parse (op,fl) rem
| "-no-start" :: rem -> no_start:=true; parse (op, fl) rem
| "-echo" :: rem -> echo := true ; parse (op,fl) rem
- | ("-v8"|"-full" as o) :: rem ->
- Printf.eprintf "warning: option %s deprecated\n" o; parse (op,fl) rem
(* Extra options with arity 0 or 1, directly passed to ocamlc/ocamlopt *)
| ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem ->
@@ -189,6 +189,7 @@ let parse_args () =
end
| ("-h"|"-help"|"--help") :: _ -> usage ()
+ | f :: rem when supported_flambda_option f -> parse (op,fl) rem
| f :: rem when supported_suffix f -> parse (op,f::fl) rem
| f :: _ -> prerr_endline ("Don't know what to do with " ^ f); exit 1
in
@@ -254,6 +255,17 @@ let create_tmp_main_file modules =
with reraise ->
clean main_name; raise reraise
+(* TODO: remove once OCaml 4.04 is adopted *)
+let split_on_char sep s =
+ let r = ref [] in
+ let j = ref (String.length s) in
+ for i = String.length s - 1 downto 0 do
+ if s.[i] = sep then begin
+ r := String.sub s (i + 1) (!j - i - 1) :: !r;
+ j := i
+ end
+ done;
+ String.sub s 0 !j :: !r
(** {6 Main } *)
@@ -266,15 +278,17 @@ let main () =
let prog = if !opt then "opt" else "ocamlc" in
(* Which arguments ? *)
if !opt && !top then failwith "no custom toplevel in native code!";
- let flags = if !opt then [] else Coq_config.vmbyteflags in
+ let flags = if !opt then Coq_config.flambda_flags else Coq_config.vmbyteflags in
let topstart = if !top then [ "topstart.cmo" ] else [] in
let (modules, tolink) = files_to_link userfiles in
let main_file = create_tmp_main_file modules in
try
(* - We add topstart.cmo explicitly because we shunted ocamlmktop wrapper.
- With the coq .cma, we MUST use the -linkall option. *)
+ let coq_camlflags =
+ List.filter ((<>) "") (split_on_char ' ' Coq_config.caml_flags) in
let args =
- "-linkall" :: "-rectypes" :: "-w" :: "-31" :: flags @ copts @ options @
+ coq_camlflags @ "-linkall" :: "-w" :: "-31" :: flags @ copts @ options @
(std_includes basedir) @ tolink @ [ main_file ] @ topstart
in
if !echo then begin
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index a0b6bfbbed..6ddeeb9b28 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -94,7 +94,7 @@ let rcs = "\036" rcs_keyword [^ '$']* "\036"
let stars = "(*" '*'* "*)"
let dot = '.' (' ' | '\t' | '\n' | '\r' | eof)
let proof_start =
- "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" | "Next"
+ "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" space+ (['0' - '9'])+ | "Next" space+ "Obligation"
let def_start =
"Definition" | "Fixpoint" | "Instance"
let proof_end =
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index a9da27ba23..79723431cf 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -252,11 +252,9 @@ let eval_print l coq =
let to_id, _ = get_id id in
eval_call (query (0,(phrase, to_id))) coq
| [ Tok(_,"WAIT") ] ->
- let phrase = "Stm Wait." in
- eval_call (query (0,(phrase,tip_id()))) coq
+ eval_call (wait ()) coq
| [ Tok(_,"JOIN") ] ->
- let phrase = "Stm JoinDocument." in
- eval_call (query (0,(phrase,tip_id()))) coq
+ eval_call (status true) coq
| [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] ->
let to_id, _ = get_id id in
if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip"
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 22:55:38 +0000