diff options
39 files changed, 141 insertions, 137 deletions
diff --git a/.bintray.json b/.bintray.json deleted file mode 100644 index 1b32a144c8..0000000000 --- a/.bintray.json +++ /dev/null @@ -1,20 +0,0 @@ -{ - "package": { - "name": "coq", - "repo": "coq", - "subject": "coq" - }, - - "version": { - "name": "8.10+alpha" - }, - - "files": - [ - {"includePattern": "_build/(.*\\.dmg)", "uploadPattern": "$1", - "matrixParams": { - "override": 1 } - } - ], - "publish": true -} diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index fac5abf13f..77e34d4e00 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -524,7 +524,6 @@ validate:quick: library:ci-bedrock2: <<: *ci-template - allow_failure: true library:ci-color: <<: *ci-template-flambda @@ -93,10 +93,12 @@ To be effective, bug reports should mention the OCaml version used to compile and run Coq, the Coq version (`coqtop -v`), the configuration used, and include a complete source example leading to the bug. -## Contributing +## Contributing to Coq Guidelines for contributing to Coq in various ways are listed in the [contributor's guide](CONTRIBUTING.md). +Information about the next release is at https://github.com/coq/coq/wiki/Release-Plan + ## Supporting Coq Help the Coq community grow and prosper by becoming a sponsor! The [Coq diff --git a/checker/checker.ml b/checker/checker.ml index d97ab5409e..af8d1e5617 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -319,6 +319,8 @@ let explain_exn = function let deprecated flag = Feedback.msg_warning (str "Deprecated flag " ++ quote (str flag)) +let boot_opt = ref false + let parse_args argv = let rec parse = function | [] -> () @@ -348,14 +350,14 @@ let parse_args argv = | "-debug" :: rem -> set_debug (); parse rem | "-where" :: _ -> - Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); + Envars.set_coqlib ~boot:!boot_opt ~fail:(fun x -> CErrors.user_err Pp.(str x)); print_endline (Envars.coqlib ()); exit 0 | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () | ("-v"|"--version") :: _ -> version () - | "-boot" :: rem -> Flags.boot := true; parse rem + | "-boot" :: rem -> boot_opt := true; parse rem | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem | ("-o" | "--output-context") :: rem -> Check_stat.output_context := true; parse rem @@ -384,7 +386,7 @@ let init_with_argv argv = try parse_args argv; if !Flags.debug then Printexc.record_backtrace true; - Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); + Envars.set_coqlib ~boot:!boot_opt ~fail:(fun x -> CErrors.user_err Pp.(str x)); Flags.if_verbose print_header (); init_load_path (); make_senv () diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh index 5205946261..2ac78d3c2b 100755 --- a/dev/ci/ci-bedrock2.sh +++ b/dev/ci/ci-bedrock2.sh @@ -6,4 +6,4 @@ ci_dir="$(dirname "$0")" FORCE_GIT=1 git_download bedrock2 -( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && make ) +( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make ) diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 5eac3e2b9c..4d874cdd12 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -161,6 +161,7 @@ val ppobj : Libobject.obj -> unit val cast_kind_display : Constr.cast_kind -> string val constr_display : Constr.constr -> unit val print_pure_constr : Constr.types -> unit +val print_pure_econstr : EConstr.types -> unit val pploc : Loc.t -> unit diff --git a/gramlib/ploc.ml b/gramlib/ploc.ml index 9342fc6c1d..056a2b7ad3 100644 --- a/gramlib/ploc.ml +++ b/gramlib/ploc.ml @@ -6,17 +6,16 @@ open Loc let make_unlined (bp, ep) = {fname = InFile ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; - bp = bp; ep = ep; comm = ""; ecomm = ""} + bp = bp; ep = ep; } let dummy = {fname = InFile ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; - bp = 0; ep = 0; comm = ""; ecomm = ""} + bp = 0; ep = 0; } (* *) let sub loc sh len = {loc with bp = loc.bp + sh; ep = loc.bp + sh + len} let after loc sh len = {loc with bp = loc.ep + sh; ep = loc.ep + sh + len} -let with_comment loc comm = {loc with comm = comm} exception Exc of Loc.t * exn diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli index 100fbc7271..15a5a74455 100644 --- a/gramlib/ploc.mli +++ b/gramlib/ploc.mli @@ -35,6 +35,3 @@ val after : Loc.t -> int -> int -> Loc.t (** [Ploc.after loc sh len] is the location just after loc (starting at the end position of [loc]) shifted with [sh] characters and of length [len]. *) - -val with_comment : Loc.t -> string -> Loc.t - (** Change the comment part of the given location *) diff --git a/ide/idetop.ml b/ide/idetop.ml index e157696294..608577b297 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -93,23 +93,22 @@ let add ((s,eid),(sid,verbose)) = let pa = Pcoq.Parsable.make (Stream.of_string s) in match Stm.parse_sentence ~doc sid ~entry:Pvernac.main_entry pa with | None -> assert false (* s is not an empty string *) - | Some (loc, ast) -> - let loc_ast = CAst.make ~loc ast in - ide_cmd_checks ~last_valid:sid loc_ast; - let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in - set_doc doc; - let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in - ide_cmd_warns ~id:newid loc_ast; - (* TODO: the "" parameter is a leftover of the times the protocol - * used to include stderr/stdout output. - * - * Currently, we force all the output meant for the to go via the - * feedback mechanism, and we don't manipulate stderr/stdout, which - * are left to the client's discrection. The parameter is still there - * as not to break the core protocol for this minor change, but it should - * be removed in the next version of the protocol. - *) - newid, (rc, "") + | Some ast -> + ide_cmd_checks ~last_valid:sid ast; + let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose ast in + set_doc doc; + let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in + ide_cmd_warns ~id:newid ast; + (* TODO: the "" parameter is a leftover of the times the protocol + * used to include stderr/stdout output. + * + * Currently, we force all the output meant for the to go via the + * feedback mechanism, and we don't manipulate stderr/stdout, which + * are left to the client's discrection. The parameter is still there + * as not to break the core protocol for this minor change, but it should + * be removed in the next version of the protocol. + *) + newid, (rc, "") let edit_at id = let doc = get_doc () in @@ -136,9 +135,9 @@ let annotate phrase = let pa = Pcoq.Parsable.make (Stream.of_string phrase) in match Stm.parse_sentence ~doc (Stm.get_current_state ~doc) ~entry:Pvernac.main_entry pa with | None -> Richpp.richpp_of_pp 78 (Pp.mt ()) - | Some (_, ast) -> - (* XXX: Width should be a parameter of annotate... *) - Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast) + | Some ast -> + (* XXX: Width should be a parameter of annotate... *) + Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast.CAst.v) (** Goal display *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 474ce3e871..18a257047d 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1114,7 +1114,7 @@ let start_library dir senv = modvariant = LIBRARY; required = senv.required } -let export ?except senv dir = +let export ?except ~output_native_objects senv dir = let senv = try join_safe_environment ?except senv with e -> @@ -1136,7 +1136,7 @@ let export ?except senv dir = } in let ast, symbols = - if !Flags.output_native_objects then + if output_native_objects then Nativelibrary.dump_library mp dir senv.env str else [], Nativecode.empty_symbols in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 1b7239da23..8539fdd504 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -187,7 +187,7 @@ val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.sym val start_library : DirPath.t -> ModPath.t safe_transformer val export : - ?except:Future.UUIDSet.t -> + ?except:Future.UUIDSet.t -> output_native_objects:bool -> safe_environment -> DirPath.t -> ModPath.t * compiled_library * native_library diff --git a/lib/envars.ml b/lib/envars.ml index b5036e7340..8a75d9a552 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -110,11 +110,11 @@ let set_user_coqlib path = coqlib := Some path (** coqlib is now computed once during coqtop initialization *) -let set_coqlib ~fail = +let set_coqlib ~boot ~fail = match !coqlib with | Some _ -> () | None -> - let lib = if !Flags.boot then coqroot else guess_coqlib fail in + let lib = if boot then coqroot else guess_coqlib fail in coqlib := Some lib let coqlib () = Option.default "" !coqlib diff --git a/lib/envars.mli b/lib/envars.mli index ebf86d0650..21365c48f6 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -39,7 +39,7 @@ val datadir : unit -> string val configdir : unit -> string (** [set_coqlib] must be runned once before any access to [coqlib] *) -val set_coqlib : fail:(string -> string) -> unit +val set_coqlib : boot:bool -> fail:(string -> string) -> unit (** [set_user_coqlib path] sets the coqlib directory explicitedly. *) val set_user_coqlib : string -> unit diff --git a/lib/flags.ml b/lib/flags.ml index 29406ef275..768d359cce 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -41,8 +41,6 @@ let with_options ol f x = let () = List.iter2 (:=) ol vl in Exninfo.iraise reraise -let boot = ref false - let record_aux_file = ref false let test_mode = ref false @@ -118,8 +116,5 @@ let inline_level = ref default_inline_level let set_inline_level = (:=) inline_level let get_inline_level () = !inline_level -(* Native code compilation for conversion and normalization *) -let output_native_objects = ref false - let profile_ltac = ref false let profile_ltac_cutoff = ref 2.0 diff --git a/lib/flags.mli b/lib/flags.mli index b9c5e20f47..4ef5fb4445 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -31,8 +31,6 @@ (** Command-line flags *) -val boot : bool ref - (** Set by coqtop to tell the kernel to output to the aux file; will be eventually removed by cleanups such as PR#1103 *) val record_aux_file : bool ref @@ -112,9 +110,6 @@ val set_inline_level : int -> unit val get_inline_level : unit -> int val default_inline_level : int -(** When producing vo objects, also compile the native-code version *) -val output_native_objects : bool ref - (** Global profile_ltac flag *) val profile_ltac : bool ref val profile_ltac_cutoff : float ref diff --git a/lib/loc.ml b/lib/loc.ml index c08648911b..66b7a7da70 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -22,19 +22,17 @@ type t = { bol_pos_last : int; (** position of the beginning of end line *) bp : int; (** start position *) ep : int; (** end position *) - comm : string; (** start comment *) - ecomm : string (** end comment *) } let create fname line_nb bol_pos bp ep = { fname = fname; line_nb = line_nb; bol_pos = bol_pos; line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; - comm = ""; ecomm = "" } +} let make_loc (bp, ep) = { fname = ToplevelInput; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; bp = bp; ep = ep; - comm = ""; ecomm = "" } +} let mergeable loc1 loc2 = loc1.fname = loc2.fname @@ -50,7 +48,7 @@ let merge loc1 loc2 = line_nb_last = loc2.line_nb_last; bol_pos_last = loc2.bol_pos_last; bp = loc1.bp; ep = loc2.ep; - comm = loc1.comm; ecomm = loc2.comm } + } else loc1 else if loc2.ep < loc1.ep then { fname = loc2.fname; @@ -59,7 +57,6 @@ let merge loc1 loc2 = line_nb_last = loc1.line_nb_last; bol_pos_last = loc1.bol_pos_last; bp = loc2.bp; ep = loc1.ep; - comm = loc2.comm; ecomm = loc1.comm } else loc2 diff --git a/lib/loc.mli b/lib/loc.mli index c46311b639..23df1ebd9a 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -22,8 +22,6 @@ type t = { bol_pos_last : int; (** position of the beginning of end line *) bp : int; (** start position *) ep : int; (** end position *) - comm : string; (** start comment *) - ecomm : string (** end comment *) } (** {5 Location manipulation} *) diff --git a/library/declaremods.ml b/library/declaremods.ml index 8699583cdf..5fd11e187a 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -928,10 +928,10 @@ let append_end_library_hook f = let old_f = !end_library_hook in end_library_hook := fun () -> old_f(); f () -let end_library ?except dir = +let end_library ?except ~output_native_objects dir = !end_library_hook(); let oname = Lib.end_compilation_checks dir in - let mp,cenv,ast = Global.export ?except dir in + let mp,cenv,ast = Global.export ?except ~output_native_objects dir in let prefix, lib_stack = Lib.end_compilation oname in assert (ModPath.equal mp (MPfile dir)); let substitute, keep, _ = Lib.classify_segment lib_stack in diff --git a/library/declaremods.mli b/library/declaremods.mli index 7aa4bc30ce..2b28ba908e 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -99,7 +99,7 @@ val get_library_native_symbols : library_name -> Nativecode.symbols val start_library : library_name -> unit val end_library : - ?except:Future.UUIDSet.t -> library_name -> + ?except:Future.UUIDSet.t -> output_native_objects:bool -> library_name -> Safe_typing.compiled_library * library_objects * Safe_typing.native_library (** append a function to be executed at end_library *) diff --git a/library/global.ml b/library/global.ml index 784a02449c..cf996ce644 100644 --- a/library/global.ml +++ b/library/global.ml @@ -143,7 +143,8 @@ let mind_of_delta_kn kn = (** Operations on libraries *) let start_library dir = globalize (Safe_typing.start_library dir) -let export ?except s = Safe_typing.export ?except (safe_env ()) s +let export ?except ~output_native_objects s = + Safe_typing.export ?except ~output_native_objects (safe_env ()) s let import c u d = globalize (Safe_typing.import c u d) diff --git a/library/global.mli b/library/global.mli index df18625a5f..4e2ad92717 100644 --- a/library/global.mli +++ b/library/global.mli @@ -108,7 +108,7 @@ val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ. (** {6 Compiled libraries } *) val start_library : DirPath.t -> ModPath.t -val export : ?except:Future.UUIDSet.t -> DirPath.t -> +val export : ?except:Future.UUIDSet.t -> output_native_objects:bool -> DirPath.t -> ModPath.t * Safe_typing.compiled_library * Safe_typing.native_library val import : Safe_typing.compiled_library -> Univ.ContextSet.t -> Safe_typing.vodigest -> diff --git a/library/library.ml b/library/library.ml index 9b9bd07c93..37dadadb76 100644 --- a/library/library.ml +++ b/library/library.ml @@ -657,7 +657,7 @@ let error_recursively_dependent_library dir = (* Security weakness: file might have been changed on disk between writing the content and computing the checksum... *) -let save_library_to ?todo dir f otab = +let save_library_to ?todo ~output_native_objects dir f otab = let except = match todo with | None -> (* XXX *) @@ -668,7 +668,7 @@ let save_library_to ?todo dir f otab = assert(Filename.check_suffix f ".vio"); List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty l in - let cenv, seg, ast = Declaremods.end_library ~except dir in + let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in let tasks, utab, dtab = match todo with @@ -716,7 +716,7 @@ let save_library_to ?todo dir f otab = System.marshal_out_segment f' ch (opaque_table : seg_proofs); close_out ch; (* Writing native code files *) - if !Flags.output_native_objects then + if output_native_objects then let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in if not (Nativelib.compile_library dir ast fn) then user_err Pp.(str "Could not compile the library to native code.") diff --git a/library/library.mli b/library/library.mli index c016352808..a976be0184 100644 --- a/library/library.mli +++ b/library/library.mli @@ -38,9 +38,11 @@ type seg_proofs = Constr.constr Future.computation array an export otherwise just a simple import *) val import_module : bool -> qualid list -> unit -(** End the compilation of a library and save it to a ".vo" file *) +(** End the compilation of a library and save it to a ".vo" file. + [output_native_objects]: when producing vo objects, also compile the native-code version. *) val save_library_to : ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) -> + output_native_objects:bool -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit val load_library_todo : diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index be8ef24a09..73b9ef7da0 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -128,11 +128,13 @@ module Make(T : Task) () = struct | ("-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl (* Options to discard: 1 argument *) - | ("-async-proofs" |"-vio2vo" | "-o" - |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv" - |"-compile" |"-compile-verbose" - |"-async-proofs-cache" - |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl -> + | ( "-async-proofs" | "-vio2vo" | "-o" + | "-load-vernac-source" | "-l" | "-load-vernac-source-verbose" | "-lv" + | "-compile" | "-compile-verbose" + | "-async-proofs-cache" | "-async-proofs-j" | "-async-proofs-tac-j" + | "-async-proofs-private-flags" | "-async-proofs-tactic-error-resilience" + | "-async-proofs-command-error-resilience" | "-async-proofs-delegation-threshold" + | "-async-proofs-worker-priority" | "-worker-id") :: _ :: tl -> set_slave_opt tl (* We need to pass some options with one argument *) | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" | "-compat" diff --git a/stm/stm.ml b/stm/stm.ml index 0165b3c029..b4f26570c6 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2647,6 +2647,10 @@ type stm_init_options = { some point. *) doc_type : stm_doc_type; + (* Allow compiling modules in the Coq prefix. Irrelevant in + interactive mode. *) + allow_coq_overwrite : bool; + (* Initial load path in scope for the document. Usually extracted from -R options / _CoqProject *) iload_path : Mltop.coq_path list; @@ -2674,11 +2678,12 @@ let init_core () = if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true; State.register_root_state () -let check_coq_overwriting p = +let check_coq_overwriting ~allow_coq_overwrite p = + if not allow_coq_overwrite then let l = DirPath.repr p in let id, l = match l with id::l -> id,l | [] -> assert false in let is_empty = match l with [] -> true | _ -> false in - if not !Flags.boot && not is_empty && Id.equal (CList.last l) Libnames.coq_root then + if not is_empty && Id.equal (CList.last l) Libnames.coq_root then user_err (str "Cannot build module " ++ DirPath.print p ++ str "." ++ spc () ++ str "it starts with prefix \"Coq\" which is reserved for the Coq library.") @@ -2695,7 +2700,7 @@ let dirpath_of_file f = let ldir = Libnames.add_dirpath_suffix ldir0 id in ldir -let new_doc { doc_type ; iload_path; require_libs; stm_options } = +let new_doc { doc_type ; allow_coq_overwrite; iload_path; require_libs; stm_options } = let load_objs libs = let rq_file (dir, from, exp) = @@ -2730,14 +2735,14 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = | VoDoc f -> let ldir = dirpath_of_file f in - check_coq_overwriting ldir; + check_coq_overwriting ~allow_coq_overwrite ldir; let () = Flags.verbosely Declaremods.start_library ldir in VCS.set_ldir ldir; set_compilation_hints f | VioDoc f -> let ldir = dirpath_of_file f in - check_coq_overwriting ldir; + check_coq_overwriting ~allow_coq_overwrite ldir; let () = Flags.verbosely Declaremods.start_library ldir in VCS.set_ldir ldir; set_compilation_hints f @@ -2885,11 +2890,12 @@ let handle_failure (e, info) vcs = VCS.print (); Exninfo.iraise (e, info) -let snapshot_vio ~doc ldir long_f_dot_vo = +let snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vo = let doc = finish ~doc in if List.length (VCS.branches ()) > 1 then CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs"); - Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo + Library.save_library_to ~todo:(dump_snapshot ()) ~output_native_objects + ldir long_f_dot_vo (Global.opaque_tables ()); doc @@ -3197,12 +3203,12 @@ let query ~doc ~at ~route s = let rec loop () = match parse_sentence ~doc at ~entry:Pvernac.main_entry s with | None -> () - | Some (loc, ast) -> - let indentation, strlen = compute_indentation ~loc at in + | Some {CAst.loc; v=ast} -> + let indentation, strlen = compute_indentation ?loc at in let st = State.get_cached at in let aast = { verbose = true; indentation; strlen; - loc = Some loc; expr = ast } in + loc; expr = ast } in ignore(stm_vernac_interp ~route at st aast); loop () in diff --git a/stm/stm.mli b/stm/stm.mli index 821ab59a43..102e832d3e 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -67,6 +67,10 @@ type stm_init_options = { some point. *) doc_type : stm_doc_type; + (* Allow compiling modules in the Coq prefix. Irrelevant in + interactive mode. *) + allow_coq_overwrite : bool; + (* Initial load path in scope for the document. Usually extracted from -R options / _CoqProject *) iload_path : Mltop.coq_path list; @@ -156,7 +160,7 @@ val join : doc:doc -> doc - if the worker proof is not empty, then it waits until all workers are done with their current jobs and then dumps (or fails if one of the completed tasks is a failure) *) -val snapshot_vio : doc:doc -> DirPath.t -> string -> doc +val snapshot_vio : doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc (* Empties the task queue, can be used only if the worker pool is empty (E.g. * after having built a .vio in batch mode *) diff --git a/test-suite/stm/arg_filter_1.v b/test-suite/stm/arg_filter_1.v new file mode 100644 index 0000000000..1cf66d6b43 --- /dev/null +++ b/test-suite/stm/arg_filter_1.v @@ -0,0 +1,4 @@ +(* coq-prog-args: ("-async-proofs-tac-j" "1") *) + +Lemma foo : True. +Proof. now auto. Qed. diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 5fd894e908..5526970d3f 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -431,7 +431,7 @@ let _ = check_overlapping_include project; - Envars.set_coqlib ~fail:(fun x -> Printf.eprintf "Error: %s\n" x; exit 1); + Envars.set_coqlib ~boot:false ~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/coqdep.ml b/tools/coqdep.ml index 4e80caa4cc..5f8cc99ed1 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -530,7 +530,8 @@ let coqdep () = 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 -> raise (CoqlibError msg)); + (* option_boot is actually always false in this branch *) + Envars.set_coqlib ~boot:!option_boot ~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"]; diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index df2b983029..8064ee8880 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -96,6 +96,9 @@ let compile opts copts ~echo ~f_in ~f_out = let iload_path = build_load_path opts in let require_libs = require_libs opts in let stm_options = opts.stm_flags in + let output_native_objects = match opts.native_compiler with + | NativeOff -> false | NativeOn {ondemand} -> not ondemand + in match copts.compilation_mode with | BuildVo -> Flags.record_aux_file := true; @@ -109,6 +112,7 @@ let compile opts copts ~echo ~f_in ~f_out = let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) Stm.new_doc Stm.{ doc_type = VoDoc long_f_dot_vo; + allow_coq_overwrite = opts.boot; iload_path; require_libs; stm_options; } in let state = { doc; sid; proof = None; time = opts.time } in @@ -125,7 +129,7 @@ let compile opts copts ~echo ~f_in ~f_out = let _doc = Stm.join ~doc:state.doc in let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); - Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ()); + Library.save_library_to ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ()); Aux_file.record_in_aux_at "vo_compile_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); Aux_file.stop_aux_file (); @@ -159,6 +163,7 @@ let compile opts copts ~echo ~f_in ~f_out = let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) Stm.new_doc Stm.{ doc_type = VioDoc long_f_dot_vio; + allow_coq_overwrite = opts.boot; iload_path; require_libs; stm_options; } in @@ -168,7 +173,7 @@ let compile opts copts ~echo ~f_in ~f_out = let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in let doc = Stm.finish ~doc:state.doc in check_pending_proofs (); - let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in + let () = ignore (Stm.snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vio) in Stm.reset_task_queue () | Vio2Vo -> diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 74c016101a..b549f22119 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -33,8 +33,12 @@ let set_type_in_type () = type color = [`ON | `AUTO | `OFF] +type native_compiler = NativeOff | NativeOn of { ondemand : bool } + type t = { + boot : bool; + load_init : bool; load_rcfile : bool; rcfile : string option; @@ -54,7 +58,7 @@ type t = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; enable_VM : bool; - enable_native_compiler : bool; + native_compiler : native_compiler; stm_flags : Stm.AsyncOpts.stm_opt; debug : bool; @@ -79,8 +83,15 @@ type t = { let default_toplevel = Names.(DirPath.make [Id.of_string "Top"]) +let default_native = + if Coq_config.native_compiler + then NativeOn {ondemand=true} + else NativeOff + let default = { + boot = false; + load_init = true; load_rcfile = true; rcfile = None; @@ -99,7 +110,8 @@ let default = { impredicative_set = Declarations.PredicativeSet; indices_matter = false; enable_VM = true; - enable_native_compiler = Coq_config.native_compiler; + native_compiler = default_native; + stm_flags = Stm.AsyncOpts.default_opts; debug = false; diffs_set = false; @@ -232,9 +244,9 @@ let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesy exception NoCoqLib -let usage help = +let usage ~boot help = begin - try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib) + try Envars.set_coqlib ~boot ~fail:(fun x -> raise NoCoqLib) with NoCoqLib -> usage_no_coqlib () end; let lp = Coqinit.toplevel_init_load_path () in @@ -414,15 +426,14 @@ let parse_args ~help ~init arglist : t * string list = produced artifact(s) (`.vo`, `.vio`, `.coq-native`, ...) should be done by a separate flag, and the "ondemand" value removed. Once this is done, use [get_bool] here. *) - let (enable,precompile) = + let native_compiler = match (next ()) with - | ("yes" | "on") -> true, true - | "ondemand" -> true, false - | ("no" | "off") -> false, false + | ("yes" | "on") -> NativeOn {ondemand=false} + | "ondemand" -> NativeOn {ondemand=true} + | ("no" | "off") -> NativeOff | _ -> prerr_endline ("Error: (yes|no|ondemand) expected after option -native-compiler"); exit 1 in - Flags.output_native_objects := precompile; - { oval with enable_native_compiler = enable } + { oval with native_compiler } (* Options with zero arg *) |"-async-queries-always-delegate" @@ -436,7 +447,7 @@ let parse_args ~help ~init arglist : t * string list = { oval with batch = true } |"-test-mode" -> Flags.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval - |"-boot" -> Flags.boot := true; { oval with load_rcfile = false; } + |"-boot" -> { oval with boot = true; load_rcfile = false; } |"-bt" -> Backtrace.record_backtrace true; oval |"-color" -> set_color oval (next ()) |"-config"|"--config" -> { oval with print_config = true } @@ -468,7 +479,7 @@ let parse_args ~help ~init arglist : t * string list = |"-type-in-type" -> set_type_in_type (); oval |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) |"-where" -> { oval with print_where = true } - |"-h"|"-H"|"-?"|"-help"|"--help" -> usage help; oval + |"-h"|"-H"|"-?"|"-help"|"--help" -> usage ~boot:oval.boot help; oval |"-v"|"--version" -> Usage.version (exitcode oval) |"-print-version"|"--print-version" -> Usage.machine_readable_version (exitcode oval) diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index c9a7a0fd56..9cc846edea 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -12,8 +12,12 @@ type color = [`ON | `AUTO | `OFF] val default_toplevel : Names.DirPath.t +type native_compiler = NativeOff | NativeOn of { ondemand : bool } + type t = { + boot : bool; + load_init : bool; load_rcfile : bool; rcfile : string option; @@ -32,7 +36,8 @@ type t = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; enable_VM : bool; - enable_native_compiler : bool; + native_compiler : native_compiler; + stm_flags : Stm.AsyncOpts.stm_opt; debug : bool; diffs_set : bool; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 6ef0aa390d..c2c538edea 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -162,7 +162,7 @@ let init_toplevel ~help ~init custom_init arglist = (* If we have been spawned by the Spawn module, this has to be done * early since the master waits us to connect back *) Spawned.init_channels (); - Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); + Envars.set_coqlib ~boot:opts.boot ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); if opts.print_where then begin print_endline (Envars.coqlib ()); exit (exitcode opts) @@ -188,7 +188,7 @@ let init_toplevel ~help ~init custom_init arglist = Global.set_engagement opts.impredicative_set; Global.set_indices_matter opts.indices_matter; Global.set_VM opts.enable_VM; - Global.set_native_compiler opts.enable_native_compiler; + Global.set_native_compiler (match opts.native_compiler with NativeOff -> false | NativeOn _ -> true); (* Allow the user to load an arbitrary state here *) inputstate opts; @@ -221,6 +221,7 @@ let init_toploop opts = let doc, sid = Stm.(new_doc { doc_type = Interactive opts.toplevel_name; + allow_coq_overwrite = true; (* irrelevant *) iload_path; require_libs; stm_options; }) in let state = { doc; sid; proof = None; time = opts.time } in diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg index 7f1cca277e..f2025858d7 100644 --- a/toplevel/g_toplevel.mlg +++ b/toplevel/g_toplevel.mlg @@ -41,7 +41,7 @@ GRAMMAR EXTEND Gram | cmd = Pvernac.Vernac_.main_entry -> { match cmd with | None -> None - | Some (loc,c) -> Some (CAst.make ~loc (VernacControl c)) } + | Some {CAst.loc; v} -> Some (CAst.make ?loc (VernacControl v)) } ] ] ; diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 277f8b7367..0d17218a56 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -62,7 +62,7 @@ let print_usage_common co command = \n\ \n -q skip loading of rcfile\ \n -init-file f set the rcfile to f\ -\n -boot boot mode (allows to overload the `Coq` library prefix)\ +\n -boot boot mode (allows to overload the `Coq` library prefix, implies -q)\ \n -bt print backtraces (requires configure debug flag)\ \n -debug debug mode (implies -bt)\ \n -diffs (on|off|removed) highlight differences between proof steps\ diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 45ca658857..ef1dc6993b 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -101,20 +101,18 @@ let load_vernac_core ~echo ~check ~interactive ~state file = ~doc:state.doc ~entry:Pvernac.main_entry state.sid in_pa with | None -> - input_cleanup (); - state, ids, Pcoq.Parsable.comment_state in_pa - | Some (loc, ast) -> - let ast = CAst.make ~loc ast in + input_cleanup (); + state, ids, Pcoq.Parsable.comment_state in_pa + | Some ast -> + (* Printing of AST for -compile-verbose *) + Option.iter (vernac_echo ?loc:ast.CAst.loc) in_echo; - (* Printing of AST for -compile-verbose *) - Option.iter (vernac_echo ~loc) in_echo; + checknav_simple ast; - checknav_simple ast; + let state = + Flags.silently (interp_vernac ~check ~interactive ~state) ast in - let state = - Flags.silently (interp_vernac ~check ~interactive ~state) ast in - - loop state (state.sid :: ids) + loop state (state.sid :: ids) in try loop state [] with any -> (* whatever the exception *) diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index 0e46df2320..994fad85f0 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -52,7 +52,7 @@ module Vernac_ = let () = let open Extend in - let act_vernac v loc = Some (loc, v) in + let act_vernac v loc = Some CAst.(make ~loc v) in let act_eoi _ loc = None in let rule = [ Rule (Next (Stop, Atoken Tok.EOI), act_eoi); diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index fa251281dc..4bf7c9f7bd 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -26,7 +26,7 @@ module Vernac_ : val rec_definition : (fixpoint_expr * decl_notation list) Entry.t val noedit_mode : vernac_expr Entry.t val command_entry : vernac_expr Entry.t - val main_entry : (Loc.t * vernac_control) option Entry.t + val main_entry : vernac_control CAst.t option Entry.t val red_expr : raw_red_expr Entry.t val hint_info : Hints.hint_info_expr Entry.t end @@ -40,7 +40,7 @@ module Unsafe : sig end (** The main entry: reads an optional vernac command *) -val main_entry : proof_mode option -> (Loc.t * vernac_control) option Entry.t +val main_entry : proof_mode option -> vernac_control CAst.t option Entry.t (** Grammar entry for tactics: proof mode(s). By default Coq's grammar has an empty entry (non-terminal) for diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index eb263757e2..fcb96401ee 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2150,7 +2150,7 @@ let vernac_load interp fname = else None in - interp (snd (parse_sentence proof_mode input)); + interp (parse_sentence proof_mode input).CAst.v; done with End_of_input -> () end; |