aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in17
-rw-r--r--tools/coq_makefile.ml3
-rw-r--r--tools/coqc.ml2
-rw-r--r--tools/coqdep_lexer.mll42
-rw-r--r--tools/coqmktop.ml15
-rw-r--r--tools/coqwc.mll2
-rw-r--r--tools/fake_ide.ml6
7 files changed, 48 insertions, 39 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 56e12a1e06..cfa5526025 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@
@@ -100,11 +101,11 @@ AFTER ?=
CAMLDONTLINK=camlp5.gramlib,unix,str
# OCaml binaries
-CAMLC ?= "$(OCAMLFIND)" ocamlc -c -rectypes -thread
-CAMLOPTC ?= "$(OCAMLFIND)" opt -c -rectypes -thread
-CAMLLINK ?= "$(OCAMLFIND)" ocamlc -rectypes -thread -linkpkg -dontlink $(CAMLDONTLINK)
-CAMLOPTLINK ?= "$(OCAMLFIND)" opt -rectypes -thread -linkpkg -dontlink $(CAMLDONTLINK)
-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
@@ -114,8 +115,6 @@ DESTDIR ?=
CAMLDEBUG ?=
COQDEBUG ?=
-# Extra flags to the OCaml compiler
-CAMLFLAGS ?=
# Extra packages to be linked in (as in findlib -package)
CAMLPKGS ?=
@@ -500,7 +499,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
@@ -749,7 +748,7 @@ printenv::
# file you can extend the merlin-hook target in @LOCAL_FILE@
.merlin:
$(SHOW)'FILL .merlin'
- $(HIDE)echo 'FLG -rectypes -thread' > .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/coq_makefile.ml b/tools/coq_makefile.ml
index de76bf98bc..4a9d871fd3 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -274,7 +274,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)
=
@@ -283,6 +283,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)
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 862225d3d1..b381c5ba42 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -93,7 +93,7 @@ let parse_args () =
| ("-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac"
|"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob"
- |"-q"|"-profile"|"-just-parsing"|"-echo" |"-quiet"
+ |"-q"|"-profile"|"-echo" |"-quiet"
|"-silent"|"-m"|"-beautify"|"-strict-implicit"
|"-impredicative-set"|"-vm"|"-native-compiler"
|"-indices-matter"|"-quick"|"-type-in-type"
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/coqmktop.ml b/tools/coqmktop.ml
index 28a3c791cb..c21db300ad 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -252,6 +252,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 } *)
@@ -271,8 +282,10 @@ let main () =
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-03-08 05:57:36 +0000