diff options
| -rw-r--r-- | .gitlab-ci.yml | 2 | ||||
| -rw-r--r-- | Makefile.build | 5 | ||||
| -rw-r--r-- | Makefile.doc | 2 | ||||
| -rw-r--r-- | checker/checker.ml | 8 | ||||
| -rw-r--r-- | doc/dune | 2 | ||||
| -rw-r--r-- | doc/tools/coqrst/repl/coqtop.py | 5 | ||||
| -rw-r--r-- | lib/envars.ml | 4 | ||||
| -rw-r--r-- | lib/envars.mli | 2 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 6 | ||||
| -rw-r--r-- | tools/coqdep.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 6 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 |
12 files changed, 23 insertions, 23 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f434b63d74..428c03a377 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -132,7 +132,7 @@ after_script: dependencies: - not-a-real-job script: - - SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/" COQBOOT=no' + - SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/"' - make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= refman - make install-doc-sphinx artifacts: diff --git a/Makefile.build b/Makefile.build index ca988aaac2..8afb498a63 100644 --- a/Makefile.build +++ b/Makefile.build @@ -198,7 +198,10 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) # TIME="%C (%U user, %S sys, %e total, %M maxres)" COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) $(COQUSERFLAGS) -BOOTCOQC=$(TIMER) $(COQC) -boot $(COQOPTS) +# Beware this depends on the makefile being in a particular dir, we +# should pass an absolute path here but windows is tricky +# c.f. https://github.com/coq/coq/pull/9560 +BOOTCOQC=$(TIMER) $(COQC) -coqlib . -boot $(COQOPTS) LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS)) MLINCLUDES=$(LOCALINCLUDES) diff --git a/Makefile.doc b/Makefile.doc index 4b2dd8ed4d..912738cd00 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -31,7 +31,7 @@ DVIPS:=dvips HTMLSTYLE:=coqremote # Sphinx-related variables -SPHINXENV:=COQBIN="$(CURDIR)/bin/" +SPHINXENV:=COQBIN="$(CURDIR)/bin/" COQLIB="$(CURDIR)" SPHINXOPTS= -j4 SPHINXWARNERROR ?= 1 ifeq ($(SPHINXWARNERROR),1) diff --git a/checker/checker.ml b/checker/checker.ml index af8d1e5617..3db7ccdcae 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -350,9 +350,9 @@ let parse_args argv = | "-debug" :: rem -> set_debug (); parse rem | "-where" :: _ -> - Envars.set_coqlib ~boot:!boot_opt ~fail:(fun x -> CErrors.user_err Pp.(str x)); - print_endline (Envars.coqlib ()); - exit 0 + Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); + print_endline (Envars.coqlib ()); + exit 0 | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () @@ -386,7 +386,7 @@ let init_with_argv argv = try parse_args argv; if !Flags.debug then Printexc.record_backtrace true; - Envars.set_coqlib ~boot:!boot_opt ~fail:(fun x -> CErrors.user_err Pp.(str x)); + Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); Flags.if_verbose print_header (); init_load_path (); make_senv () @@ -13,7 +13,7 @@ (source_tree tools) (env_var SPHINXWARNOPT)) (action - (run sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) + (run env COQLIB=%{project_root} sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) (alias (name refman-html) diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py index 3ff00eaaf3..2ee78a1675 100644 --- a/doc/tools/coqrst/repl/coqtop.py +++ b/doc/tools/coqrst/repl/coqtop.py @@ -41,13 +41,10 @@ class CoqTop: the ansicolors module) :param args: Additional arugments to coqtop. """ - BOOT = True - if os.getenv('COQBOOT') == "no": - BOOT = False self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN', ""), "coqtop") if not pexpect.utils.which(self.coqtop_bin): raise ValueError("coqtop binary not found: '{}'".format(self.coqtop_bin)) - self.args = (args or []) + ["-boot"] * BOOT + ["-color", "on"] * color + self.args = (args or []) + ["-color", "on"] * color self.coqtop = None def __enter__(self): diff --git a/lib/envars.ml b/lib/envars.ml index 8a75d9a552..0f4670688b 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 ~boot ~fail = +let set_coqlib ~fail = match !coqlib with | Some _ -> () | None -> - let lib = if boot then coqroot else guess_coqlib fail in + let lib = guess_coqlib fail in coqlib := Some lib let coqlib () = Option.default "" !coqlib diff --git a/lib/envars.mli b/lib/envars.mli index 21365c48f6..ebf86d0650 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 : boot:bool -> fail:(string -> string) -> unit +val set_coqlib : fail:(string -> string) -> unit (** [set_user_coqlib path] sets the coqlib directory explicitedly. *) val set_user_coqlib : string -> unit diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 5526970d3f..4f01a6bd87 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -424,15 +424,15 @@ let _ = end; let project = ensure_root_dir project in - + if project.install_kind <> (Some CoqProject_file.NoInstall) then begin warn_install_at_root_directory project; end; check_overlapping_include project; - Envars.set_coqlib ~boot:false ~fail:(fun x -> Printf.eprintf "Error: %s\n" x; exit 1); - + 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; close_out ocm; diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 5f8cc99ed1..66f1f257b8 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -531,7 +531,7 @@ let coqdep () = add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"]; end else begin (* option_boot is actually always false in this branch *) - Envars.set_coqlib ~boot:!option_boot ~fail:(fun msg -> raise (CoqlibError msg)); + Envars.set_coqlib ~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/coqargs.ml b/toplevel/coqargs.ml index c110f3831e..0c9201c3a5 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -251,9 +251,9 @@ let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesy exception NoCoqLib -let usage ~boot help = +let usage help = begin - try Envars.set_coqlib ~boot ~fail:(fun x -> raise NoCoqLib) + try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib) with NoCoqLib -> usage_no_coqlib () end; let lp = Coqinit.toplevel_init_load_path () in @@ -491,7 +491,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 ~boot:oval.boot help; oval + |"-h"|"-H"|"-?"|"-help"|"--help" -> usage help; oval |"-v"|"--version" -> Usage.version (exitcode oval) |"-print-version"|"--print-version" -> Usage.machine_readable_version (exitcode oval) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c2c538edea..9115fbb726 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 ~boot:opts.boot ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); + Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); if opts.print_where then begin print_endline (Envars.coqlib ()); exit (exitcode opts) |