diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 65 | ||||
| -rw-r--r-- | tools/TimeFileMaker.py | 15 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 56 | ||||
| -rw-r--r-- | tools/coqc.ml | 2 | ||||
| -rw-r--r-- | tools/coqdep_lexer.mll | 42 | ||||
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 19 | ||||
| -rw-r--r-- | tools/coqmktop.ml | 298 | ||||
| -rw-r--r-- | tools/coqwc.mll | 2 | ||||
| -rw-r--r-- | tools/coqworkmgr.ml | 8 | ||||
| -rw-r--r-- | tools/fake_ide.ml | 8 | ||||
| -rw-r--r-- | tools/inferior-coq.el (renamed from tools/coq-inferior.el) | 0 |
11 files changed, 118 insertions, 397 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index f4d1118d0f..de113df6a5 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@ @@ -86,7 +87,6 @@ COQCHK ?= "$(COQBIN)coqchk" COQDEP ?= "$(COQBIN)coqdep" GALLINA ?= "$(COQBIN)gallina" COQDOC ?= "$(COQBIN)coqdoc" -COQMKTOP ?= "$(COQBIN)coqmktop" COQMKFILE ?= "$(COQBIN)coq_makefile" # Timing scripts @@ -100,11 +100,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 +114,6 @@ DESTDIR ?= CAMLDEBUG ?= COQDEBUG ?= -# Extra flags to the OCaml compiler -CAMLFLAGS ?= # Extra packages to be linked in (as in findlib -package) CAMLPKGS ?= @@ -173,14 +171,15 @@ COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML) # The version of Coq being run and the version of coq_makefile that # generated this makefile -COQ_VERSION:=$(shell $(COQC) --print-version | cut -d ' ' -f 1) +COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1) COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") -CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) $(OCAML_API_FLAGS) +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) -CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib) +# ocamldoc fails with unknown argument otherwise +CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) # FIXME This should be generated by Coq GRAMMARS:=grammar.cma @@ -190,7 +189,12 @@ else CAMLP4EXTEND= endif +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 @@ -207,8 +211,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 @@ -223,8 +227,9 @@ COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop) # We here define a bunch of variables about the files being part of the # Coq project in order to ease the writing of build target and build rules +VDFILE := .coqdeps + ALLSRCFILES := \ - $(VFILES) \ $(ML4FILES) \ $(MLFILES) \ $(MLPACKFILES) \ @@ -284,13 +289,15 @@ ALLNATIVEFILES = \ $(OBJFILES:.o=.cmi) \ $(OBJFILES:.o=.cmx) \ $(OBJFILES:.o=.cmxs) -# trick: wildcard filters out non-existing files -NATIVEFILESTOINSTALL = $(foreach f, $(ALLNATIVEFILES), $(wildcard $f)) +# trick: wildcard filters out non-existing files, so that `install` doesn't show +# warnings and `clean` doesn't pass to rm a list of files that is too long for +# the shell. +NATIVEFILES = $(wildcard $(ALLNATIVEFILES)) FILESTOINSTALL = \ $(VOFILES) \ $(VFILES) \ $(GLOBFILES) \ - $(NATIVEFILESTOINSTALL) \ + $(NATIVEFILES) \ $(CMIFILESTOINSTALL) BYTEFILESTOINSTALL = \ $(CMOFILESTOINSTALL) \ @@ -302,7 +309,7 @@ else DO_NATDYNLINK = endif -ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) +ALLDFILES = $(addsuffix .d,$(ALLSRCFILES) $(VDFILE)) # Compilation targets ######################################################### @@ -387,7 +394,7 @@ checkproofs: .PHONY: checkproofs validate: $(VOFILES) - $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(notdir $(^:.vo=)) + $(TIMER) $(COQCHK) $(COQCHKFLAGS) $^ .PHONY: validate only: $(TGTS) @@ -405,12 +412,12 @@ mlihtml: $(MLIFILES:.mli=.cmi) $(SHOW)'CAMLDOC -d $@' $(HIDE)mkdir $@ || rm -rf $@/* $(HIDE)$(CAMLDOC) -html \ - -d $@ -m A $(CAMLDEBUG) $(CAMLFLAGS) $(MLIFILES) + -d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) all-mli.tex: $(MLIFILES:.mli=.cmi) $(SHOW)'CAMLDOC -latex $@' $(HIDE)$(CAMLDOC) -latex \ - -o $@ -m A $(CAMLDEBUG) $(CAMLFLAGS) $(MLIFILES) + -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) gallina: $(GFILES) @@ -427,7 +434,7 @@ all.pdf: $(VFILES) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` # FIXME: not quite right, since the output name is different -gallinahtml: GAL=g +gallinahtml: GAL=-g gallinahtml: html all-gal.ps: GAL=-g @@ -500,7 +507,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 @@ -530,7 +537,7 @@ clean:: $(HIDE)rm -f $(CMOFILES:.cmo=.o) $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) $(HIDE)rm -f $(ALLDFILES) - $(HIDE)rm -f $(ALLNATIVEFILES) + $(HIDE)rm -f $(NATIVEFILES) $(HIDE)find . -name .coq-native -type d -empty -delete $(HIDE)rm -f $(VOFILES) $(HIDE)rm -f $(VOFILES:.vo=.vio) @@ -558,7 +565,7 @@ cleanall:: clean archclean:: @# Extension point $(SHOW)'CLEAN *.cmx *.o' - $(HIDE)rm -f $(ALLNATIVEFILES) + $(HIDE)rm -f $(NATIVEFILES) $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) .PHONY: archclean @@ -707,9 +714,9 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack $(SHOW)'COQDEP $<' $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) -$(addsuffix .d,$(VFILES)): %.v.d: %.v - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c "$<" $(redir_if_ok) +$(VDFILE).d: $(VFILES) + $(SHOW)'COQDEP VFILES' + $(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c $(VFILES) $(redir_if_ok) # Misc ######################################################################## @@ -749,7 +756,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/TimeFileMaker.py b/tools/TimeFileMaker.py index a207c2171b..a5a5fa8fe5 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) @@ -55,12 +55,15 @@ def get_single_file_times(file_name): FORMAT = 'Chars %%0%dd - %%0%dd %%s' % (longest, longest) return dict((FORMAT % (int(start), int(stop), name), reformat_time_string(time)) for start, stop, name, time, extra in times) +def fix_sign_for_sorting(num, descending=True): + return -num if descending else num + def make_sorting_key(times_dict, descending=True): def get_key(name): minutes, seconds = times_dict[name].replace('s', '').split('m') - def fix_sign(num): - return -num if descending else num - return (fix_sign(int(minutes)), fix_sign(float(seconds)), name) + return (fix_sign_for_sorting(int(minutes), descending=descending), + fix_sign_for_sorting(float(seconds), descending=descending), + name) return get_key def get_sorted_file_list_from_times_dict(times_dict, descending=True): @@ -123,7 +126,7 @@ def make_diff_table_string(left_times_dict, right_times_dict, for name, lseconds, rseconds in prediff_times) # update to sort by approximate difference, first get_key = make_sorting_key(all_names_dict, descending=descending) - all_names_dict = dict((name, (abs(int(to_seconds(diff_times_dict[name]))), get_key(name))) + all_names_dict = dict((name, (fix_sign_for_sorting(int(abs(to_seconds(diff_times_dict[name]))), descending=descending), get_key(name))) for name in all_names_dict.keys()) names = sorted(all_names_dict.keys(), key=all_names_dict.get) #names = get_sorted_file_list_from_times_dict(all_names_dict, descending=descending) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index de76bf98bc..091869407e 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -27,16 +27,8 @@ let rec print_prefix_list sep = function | x :: l -> print sep; print x; print_prefix_list sep l | [] -> () -let usage () = - output_string stderr "Usage summary:\ -\n\ -\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\ -\n ... [any] ... [-extra[-phony] result dependencies command]\ -\n ... [-I dir] ... [-R physicalpath logicalpath]\ -\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\ -\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\ -\n [-h] [--help]\ -\n\ +let usage_common () = + output_string stderr "\ \n[file.v]: Coq file to be compiled\ \n[file.ml[i4]?]: Objective Caml file to be compiled\ \n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\ @@ -65,10 +57,28 @@ let usage () = \n[-install opt]: where opt is \"user\" to force install into user directory,\ \n \"none\" to build a makefile with no install target or\ \n \"global\" to force install in $COQLIB directory\ +\n" + +let usage_coq_project () = + output_string stderr "Available arguments:"; + usage_common (); + exit 1 + +let usage_coq_makefile () = + output_string stderr "Usage summary:\ +\n\ +\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\ +\n ... [any] ... [-extra[-phony] result dependencies command]\ +\n ... [-I dir] ... [-R physicalpath logicalpath]\ +\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\ +\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\ +\n [-h] [--help]\ +\n"; + usage_common (); + output_string stderr "\ \n[-f file]: take the contents of file as arguments\ -\n[-o file]: output should go in file file\ +\n[-o file]: output should go in file file (recommended)\ \n Output file outside the current directory is forbidden.\ -\n[-bypass-API]: when compiling plugins, bypass Coq API\ \n[-h]: print this usage summary\ \n[--help]: equivalent to [-h]\n"; exit 1 @@ -122,7 +132,8 @@ let generate_makefile oc conf_file local_file args project = 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; @@ -198,16 +209,10 @@ let windrive s = else s ;; -let generate_conf_coq_config oc args bypass_API = +let generate_conf_coq_config oc args = 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 in + let src_dirs = Coq_config.all_src_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) ;; @@ -266,7 +271,7 @@ let generate_conf oc project args = fprintf oc "# %s\n\n" (String.concat " " (List.map quote args)); generate_conf_files oc project; generate_conf_includes oc project; - generate_conf_coq_config oc args project.bypass_API; + generate_conf_coq_config oc args; generate_conf_defs oc project; generate_conf_doc oc project; generate_conf_extra_target oc project.extra_targets; @@ -274,7 +279,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 +288,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) @@ -378,8 +384,8 @@ let share_prefix s1 s2 = | _ -> false let _ = + let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in let prog, args = - if Array.length Sys.argv = 1 then usage (); let args = Array.to_list Sys.argv in let prog = List.hd args in prog, List.tl args in @@ -390,7 +396,7 @@ let _ = let project = try cmdline_args_to_project ~curdir:Filename.current_dir_name args - with Parsing_error s -> prerr_endline s; usage () in + with Parsing_error s -> prerr_endline s; usage_coq_project () in if only_destination <> None then begin destination_of project (Option.get only_destination); 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/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/coqmktop.ml b/tools/coqmktop.ml deleted file mode 100644 index 28a3c791cb..0000000000 --- a/tools/coqmktop.ml +++ /dev/null @@ -1,298 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** {1 Coqmktop} *) - -(** coqmktop is a script to link Coq, analogous to ocamlmktop. - The command line contains options specific to coqmktop, options for the - Ocaml linker and files to link (in addition to the default Coq files). *) - -(** {6 Utilities} *) - -(** Split a string at each blank -*) -let split_list = - let spaces = Str.regexp "[ \t\n]+" in - fun str -> Str.split spaces str - -[@@@ocaml.warning "-3"] (* String.uncapitalize_ascii since 4.03.0 GPR#124 *) -let capitalize = String.capitalize -[@@@ocaml.warning "+3"] - -let (/) = Filename.concat - -(** Which user files do we support (and propagate to ocamlopt) ? -*) -let supported_suffix f = match CUnix.get_extension f with - | ".ml" | ".cmx" | ".cmo" | ".cmxa" | ".cma" | ".c" -> true - | _ -> false - -(** From bytecode extension to native -*) -let native_suffix f = match CUnix.get_extension f with - | ".cmo" -> (Filename.chop_suffix f ".cmo") ^ ".cmx" - | ".cma" -> (Filename.chop_suffix f ".cma") ^ ".cmxa" - | ".a" -> f - | _ -> failwith ("File "^f^" has not extension .cmo, .cma or .a") - -(** Transforms a file name in the corresponding Caml module name. -*) -let module_of_file name = - capitalize (try Filename.chop_extension name with Invalid_argument _ -> name) - -(** Run a command [prog] with arguments [args]. - We do not use [Sys.command] anymore, see comment in [CUnix.sys_command]. -*) -let run_command prog args = - match CUnix.sys_command prog args with - | Unix.WEXITED 127 -> failwith ("no such command "^prog) - | Unix.WEXITED n -> n - | Unix.WSIGNALED n -> failwith (prog^" killed by signal "^string_of_int n) - | Unix.WSTOPPED n -> failwith (prog^" stopped by signal "^string_of_int n) - - - -(** {6 Coqmktop options} *) - -let opt = ref false -let top = ref false -let echo = ref false -let no_start = ref false - -let is_ocaml4 = Coq_config.caml_version.[0] <> '3' - -(** {6 Includes options} *) - -(** Since the Coq core .cma are given with their relative paths - (e.g. "lib/clib.cma"), we only need to include directories mentionned in - the temp main ml file below (for accessing the corresponding .cmi). *) - -let std_includes basedir = - let rebase d = match basedir with None -> d | Some base -> base / d in - ["-I"; rebase "."; - "-I"; rebase "lib"; - "-I"; rebase "vernac"; (* For Mltop *) - "-I"; rebase "toplevel"; - "-I"; rebase "kernel/byterun"; - "-I"; Envars.camlp4lib () ] @ - (if is_ocaml4 then ["-I"; "+compiler-libs"] else []) - -(** For the -R option, visit all directories under [dir] and add - corresponding -I to the [opts] option list (in reversed order) *) -let incl_all_subdirs dir opts = - let l = ref opts in - let add f = l := f :: "-I" :: !l in - let rec traverse dir = - if Sys.file_exists dir && Sys.is_directory dir then - let () = add dir in - let subdirs = try Sys.readdir dir with any -> [||] in - Array.iter (fun f -> traverse (dir/f)) subdirs - in - traverse dir; !l - - -(** {6 Objects to link} *) - -(** NB: dynlink is now always linked, it is used for loading plugins - and compiled vm code (see native-compiler). We now reject platforms - with ocamlopt but no dynlink.cmxa during ./configure, and give - instructions there about how to build a dummy dynlink.cmxa, - cf. dev/dynlink.ml. *) - -(** OCaml + CamlpX libraries *) - -let ocaml_libs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma";"threads.cma"] -let camlp4_libs = ["gramlib.cma"] -let libobjs = ocaml_libs @ camlp4_libs - -(** Toplevel objects *) - -let ocaml_topobjs = - if is_ocaml4 then - ["ocamlcommon.cma";"ocamlbytecomp.cma";"ocamltoplevel.cma"] - else - ["toplevellib.cma"] - -let camlp4_topobjs = ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"] - -let topobjs = ocaml_topobjs @ camlp4_topobjs - -(** Coq Core objects *) - -let copts = (split_list Coq_config.osdeplibs) @ (split_list Tolink.copts) -let core_objs = split_list Tolink.core_objs -let core_libs = split_list Tolink.core_libs - -(** Build the list of files to link and the list of modules names -*) -let files_to_link userfiles = - let top = if !top then topobjs else [] in - let modules = List.map module_of_file (top @ core_objs @ userfiles) in - let objs = libobjs @ top @ core_libs in - let objs' = (if !opt then List.map native_suffix objs else objs) @ userfiles - in (modules, objs') - - -(** {6 Parsing of the command-line} *) - -let usage () = - prerr_endline "Usage: coqmktop <options> <ocaml options> files\ -\nFlags are:\ -\n -coqlib dir Specify where the Coq object files are\ -\n -ocamlfind dir Specify where the ocamlfind binary is\ -\n -camlp4bin dir Specify where the Camlp4/5 binaries are\ -\n -o exec-file Specify the name of the resulting toplevel\ -\n -boot Run in boot mode\ -\n -echo Print calls to external commands\ -\n -opt Compile in native code\ -\n -top Build Coq on a OCaml toplevel (incompatible with -opt)\ -\n -R dir Add recursively dir to OCaml search path\ -\n"; - exit 1 - -let parse_args () = - let rec parse (op,fl) = function - | [] -> List.rev op, List.rev fl - - (* Directories *) - | "-coqlib" :: d :: rem -> - Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem - | "-ocamlfind" :: d :: rem -> - Flags.ocamlfind_spec := true; Flags.ocamlfind := d ; parse (op,fl) rem - | "-camlp4bin" :: d :: rem -> - Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem - | "-R" :: d :: rem -> parse (incl_all_subdirs d op,fl) rem - | ("-coqlib"|"-camlbin"|"-camlp4bin"|"-R") :: [] -> usage () - - (* Boolean options of coqmktop *) - | "-boot" :: rem -> Flags.boot := true; parse (op,fl) rem - | "-opt" :: rem -> opt := true ; parse (op,fl) rem - | "-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 - - (* Extra options with arity 0 or 1, directly passed to ocamlc/ocamlopt *) - | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem -> - parse (o::op,fl) rem - | ("-cclib"|"-ccopt"|"-I"|"-o"|"-w" as o) :: rem' -> - begin - match rem' with - | a :: rem -> parse (a::o::op,fl) rem - | [] -> usage () - end - - | ("-h"|"-help"|"--help") :: _ -> usage () - | 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 - parse ([],[]) (List.tl (Array.to_list Sys.argv)) - - -(** {6 Temporary main file} *) - -(** remove the temporary main file -*) -let clean file = - let rm f = if Sys.file_exists f then Sys.remove f in - let basename = Filename.chop_suffix file ".ml" in - if not !echo then begin - rm file; - rm (basename ^ ".o"); - rm (basename ^ ".cmi"); - rm (basename ^ ".cmo"); - rm (basename ^ ".cmx") - end - -(** Initializes the kind of loading in the main program -*) -let declare_loading_string () = - if not !top then - "Mltop.remove ();;" - else - "begin try\ -\n (* Enable rectypes in the toplevel if it has the directive #rectypes *)\ -\n begin match Hashtbl.find Toploop.directive_table \"rectypes\" with\ -\n | Toploop.Directive_none f -> f ()\ -\n | _ -> ()\ -\n end\ -\n with\ -\n | Not_found -> ()\ -\n end;;\ -\n\ -\n let ppf = Format.std_formatter;;\ -\n Mltop.set_top\ -\n {Mltop.load_obj=\ -\n (fun f -> if not (Topdirs.load_file ppf f)\ -\n then CErrors.user_err Pp.(str (\"Could not load plugin \"^f)));\ -\n Mltop.use_file=Topdirs.dir_use ppf;\ -\n Mltop.add_dir=Topdirs.dir_directory;\ -\n Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\ -\n" - -(** create a temporary main file to link -*) -let create_tmp_main_file modules = - let main_name,oc = Filename.open_temp_file "coqmain" ".ml" in - try - (* Add the pre-linked modules *) - output_string oc "List.iter Mltop.add_known_module [\""; - output_string oc (String.concat "\";\"" modules); - output_string oc "\"];;\n"; - (* Initializes the kind of loading *) - output_string oc (declare_loading_string()); - (* Start the toplevel loop *) - if not !no_start then output_string oc "Coqtop.start();;\n"; - close_out oc; - main_name - with reraise -> - clean main_name; raise reraise - - -(** {6 Main } *) - -let main () = - let (options, userfiles) = parse_args () in - (* Directories: *) - let () = Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)) in - let basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in - (* Which ocaml compiler to invoke *) - 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 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 args = - "-linkall" :: "-rectypes" :: "-w" :: "-31" :: flags @ copts @ options @ - (std_includes basedir) @ tolink @ [ main_file ] @ topstart - in - if !echo then begin - let command = String.concat " " (Envars.ocamlfind ()::prog::args) in - print_endline command; - print_endline - ("(command length is " ^ - (string_of_int (String.length command)) ^ " characters)"); - flush Pervasives.stdout - end; - let exitcode = run_command (Envars.ocamlfind ()) (prog::args) in - clean main_file; - exitcode - with reraise -> clean main_file; raise reraise - -let pr_exn = function - | Failure msg -> msg - | Unix.Unix_error (err,fn,arg) -> fn^" "^arg^" : "^Unix.error_message err - | any -> Printexc.to_string any - -let _ = - try exit (main ()) - with any -> Printf.eprintf "Error: %s\n" (pr_exn any); exit 1 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/coqworkmgr.ml b/tools/coqworkmgr.ml index e1d1c60d72..f4777c4fb7 100644 --- a/tools/coqworkmgr.ml +++ b/tools/coqworkmgr.ml @@ -14,7 +14,7 @@ type party = { sock : Unix.file_descr; cout : out_channel; mutable tokens : int; - priority : Flags.priority; + priority : priority; } let answer party msg = @@ -42,10 +42,10 @@ end = struct let is_empty q = !q = [] let rec split acc = function | [] -> List.rev acc, [] - | (_, { priority = Flags.Low }) :: _ as l -> List.rev acc, l + | (_, { priority = Low }) :: _ as l -> List.rev acc, l | x :: xs -> split (x :: acc) xs let push (_,{ priority } as item) q = - if priority = Flags.Low then q := !q @ [item] + if priority = Low then q := !q @ [item] else let high, low = split [] !q in q := high @ (item :: low) @@ -148,7 +148,7 @@ let check_alive s = | Some s -> let cout = Unix.out_channel_of_descr s in set_binary_mode_out cout true; - output_string cout (print_request (Hello Flags.Low)); flush cout; + output_string cout (print_request (Hello Low)); flush cout; output_string cout (print_request Ping); flush cout; begin match Unix.select [s] [] [] 1.0 with | [s],_,_ -> diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index a9da27ba23..b5c5b2b96d 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" @@ -290,7 +288,7 @@ let usage () = (Filename.basename Sys.argv.(0)) (Parser.print grammar)) -module Coqide = Spawn.Sync(struct end) +module Coqide = Spawn.Sync () let main = if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe diff --git a/tools/coq-inferior.el b/tools/inferior-coq.el index b79d97d66e..b79d97d66e 100644 --- a/tools/coq-inferior.el +++ b/tools/inferior-coq.el |