Merge PR coq#19927: Rocq CLI

Reviewed-by: ppedrot
Ack-by: Zimmi48
Co-authored-by: ppedrot <[email protected]>

.github/workflows/ci-macos.yml

@@ -36,15 +36,15 @@ jobs:
           eval $(opam env)
           ./configure -prefix "$(pwd)/_install_ci" -native-compiler no
           make dunestrap
-          dune build -p coq-core,rocq-core,coqide-server,coqide
+          dune build -p rocq-runtime,coq-core,rocq-core,coqide-server,coqide
         env:
           MACOSX_DEPLOYMENT_TARGET: "10.11"
           NJOBS: "2"
 
       - name: Install Coq
         run: |
           eval $(opam env)
-          dune install --prefix="$(pwd)/_install_ci" coq-core rocq-core coqide-server coqide
+          dune install --prefix="$(pwd)/_install_ci" rocq-runtime coq-core rocq-core coqide-server coqide
 
       - name: Run Coq Test Suite
         run: |

.gitlab-ci.yml

@@ -83,7 +83,7 @@ before_script:
       - config/dune.c_flags
     expire_in: 1 week
   script:
-    - PKGS=coq-core,rocq-core,coqide-server
+    - PKGS=rocq-runtime,coq-core,rocq-core,coqide-server
     - if [ "$COQIDE" != "no" ]; then PKGS=${PKGS},coqide; fi
     - dev/ci/gitlab-section.sh start coq.clean coq.clean
     - make clean # ensure that `make clean` works on a fresh clone
@@ -237,6 +237,7 @@ before_script:
   # OPAM will build out-of-tree so no point in importing artifacts
   script:
     - if [ "$COQ_CI_NATIVE" = true ]; then opam install -y coq-native; fi
+    - opam pin add --kind=path rocq-runtime.dev .
     - opam pin add --kind=path coq-core.dev .
     - opam pin add --kind=path rocq-core.dev .
     - opam pin add --kind=path coq-stdlib.dev stdlib/
@@ -341,7 +342,7 @@ build:base:dev:dune:
   script:
     - cp theories/dune.disabled theories/dune
     - cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune
-    - dune build -p coq-core,rocq-core,coqide-server
+    - dune build -p rocq-runtime,coq-core,rocq-core,coqide-server
     - ls _build/install/default/lib/coq/theories/Init/Prelude.vo
     - ls _build/install/default/lib/coq/user-contrib/Ltac2/Ltac2.vo
   only: *full-ci

INSTALL.md

@@ -91,8 +91,8 @@ To build and install Coq (and CoqIDE if desired) do:
 
     $ ./configure -prefix <install_prefix> $options
     $ make dunestrap
-    $ dune build -p coq-core,rocq-core,coq,coqide-server,coqide
-    $ dune install --prefix=<install_prefix> coq-core rocq-core coq coqide-server coqide
+    $ dune build -p rocq-runtime,coq-core,rocq-core,coq,coqide-server,coqide
+    $ dune install --prefix=<install_prefix> rocq-runtime coq-core rocq-core coq coqide-server coqide
 
 You can drop the `coqide` packages if not needed.
 

Makefile

@@ -82,7 +82,7 @@ dev-targets:
 	@echo "files that world will build. We provide some useful subtargets here:"
 	@echo ""
 	@echo "  - theories-foo: for each directory theories/Foo, build the vo files for it and set them up in _build/install/default."
-	@echo "    For instance the init target builds the prelude, combined with coq-core.install it produces a fully functional layout in _build/install/default."
+	@echo "    For instance the init target builds the prelude, combined with rocq-runtime.install it produces a fully functional layout in _build/install/default."
 
 help-install:
 	@echo ""
@@ -91,16 +91,18 @@ help-install:
 	@echo ""
 	@echo " $$ ./configure -prefix <install_prefix>"
 	@echo " $$ make dunestrap"
-	@echo " $$ dune build -p coq-core,rocq-core"
-	@echo " $$ dune install --prefix=<install_prefix> coq-core rocq-core"
+	@echo " $$ dune build -p rocq-runtime,coq-core,rocq-core"
+	@echo " $$ dune install --prefix=<install_prefix> rocq-runtime coq-core rocq-core"
 	@echo ""
 	@echo " Provided opam/dune packages are:"
 	@echo ""
-	@echo "  - coq-core: base Coq package, toplevel compilers, plugins, tools, no stdlib, no GTK"
+	@echo "  - rocq-runtime: base Rocq package, toplevel compilers, plugins, tools, no stdlib, no GTK"
+	@echo "  - coq-core: compat binaries (coqc instead of rocq compile, etc)"
 	@echo "  - rocq-core: Coq's prelude and basis of standard library"
 	@echo "  - coqide-server: XML protocol language server"
 	@echo "  - coqide: CoqIDE gtk application"
-	@echo "  - coq: meta package depending on coq-core rocq-core coq-stdlib"
+	@echo "  - coq: meta package depending on rocq-runtime coq-core rocq-core coq-stdlib"
+	@echo "    (also calls the test suite when using --with-test)"
 	@echo ""
 	@echo " To build a package, you can use:"
 	@echo ""
@@ -127,7 +129,7 @@ DUNESTRAPOPT=--root .
 
 # We regenerate always as to correctly track deps, can do better
 # We do a single call to dune as to avoid races and locking
-ifneq ($(COQ_SPLIT),) # avoid depending on local coq-core
+ifneq ($(COQ_SPLIT),) # avoid depending on local rocq-runtime
 _build/default/theories_dune_split _build/default/ltac2_dune_split .dune-stamp: FORCE
 	dune build $(DUNEOPT) $(DUNESTRAPOPT) theories_dune_split ltac2_dune_split
 	touch .dune-stamp
@@ -158,7 +160,7 @@ dunestrap: $(DUNE_FILES)
 states: dunestrap
 	dune build $(DUNEOPT) dev/shim/coqtop
 
-MAIN_TARGETS:=coq-core.install rocq-core.install coqide-server.install
+MAIN_TARGETS:=rocq-runtime.install coq-core.install rocq-core.install coqide-server.install
 
 world: dunestrap
 	dune build $(DUNEOPT) $(MAIN_TARGETS)
@@ -232,8 +234,8 @@ CONTEXT=_build/install/default
 # XXX: Port this to a dune alias so the build is hygienic!
 .PHONY: plugin-tutorial
 plugin-tutorial: dunestrap
-	dune build $(CONTEXT)/lib/coq-core/META coq-core.install theories/Init/Prelude.vo
-	+$(MAKE) OCAMLPATH=$(shell pwd)/$(CONTEXT)/lib/ COQBIN=$(shell pwd)/$(CONTEXT)/bin/ COQCORELIB=$(shell pwd)/$(CONTEXT)/lib/coq-core COQLIB=$(shell pwd)/_build/default/ -C doc/plugin_tutorial
+	dune build $(CONTEXT)/lib/rocq-runtime/META $(CONTEXT)/lib/coq-core/META rocq-runtime.install coq-core.install theories/Init/Prelude.vo
+	+$(MAKE) OCAMLPATH=$(shell pwd)/$(CONTEXT)/lib/ COQBIN=$(shell pwd)/$(CONTEXT)/bin/ COQCORELIB=$(shell pwd)/$(CONTEXT)/lib/rocq-runtime COQLIB=$(shell pwd)/_build/default/ -C doc/plugin_tutorial
 
 # This is broken in a very weird way with a permission error... see
 # the rule in doc/plugin_tutorial/dune:
@@ -276,7 +278,7 @@ $(foreach subdir,$(wildcard theories/*/),$(eval $(call subtarget,$(subdir),$(she
 
 # Other common dev targets:
 #
-# dune build coq-core.install
+# dune build rocq-runtime.install
 # dune build coq.install
 # dune build coqide.install
 #

boot/dune

@@ -2,8 +2,12 @@
 ; dependency for most Coq command line tools.
 (library
  (name boot)
- (public_name coq-core.boot)
+ (public_name rocq-runtime.boot)
  (synopsis "Coq Enviroment and Paths facilities")
  ; until ocaml/dune#4892 fixed
  ; (private_modules util)
- (libraries coq-core.config))
+ (libraries rocq-runtime.config))
+
+(deprecated_library_name
+ (old_public_name coq-core.boot)
+ (new_public_name rocq-runtime.boot))

boot/env.ml

@@ -18,7 +18,7 @@ module Path = struct
 
 end
 
-(* For now just a pointer to coq/lib (for .vo) and coq-core/lib (for plugins)  *)
+(* For now just a pointer to coq/lib (for .vo) and rocq-runtime/lib (for plugins)  *)
 type t =
   { core: Path.t
   ; lib : Path.t
@@ -52,7 +52,7 @@ let guess_coqlib () =
 let guess_coqcorelib lib =
   if Sys.file_exists (Path.relative lib plugins_dir)
   then lib
-  else Path.relative lib "../coq-core"
+  else Path.relative lib "../rocq-runtime"
 
 let fail_lib lib =
   let open Printf in
@@ -66,7 +66,7 @@ let fail_core plugin =
   let open Printf in
   eprintf "File not found: %s\n" plugin;
   eprintf "The path for Coq plugins is wrong.\n";
-  eprintf "Coq plugins are shipped in the coq-core package.\n";
+  eprintf "Coq plugins are shipped in the rocq-runtime package.\n";
   eprintf "Please check the COQCORELIB env variable.\n";
   exit 1
 

boot/env.mli

@@ -35,7 +35,7 @@ but we may do so in the future. Rules for "coqlib" are:
 - if none of the above succeeds, the initialization will fail
 
 - The [COQCORELIB] env variable is also used if set, if not, the location
-  of the coq-core files will be assumed to be [COQLIB/../coq-core], except
+  of the rocq-runtime files will be assumed to be [COQLIB/../rocq-runtime], except
   if [COQLIB/plugins] exists [as in some developers layouts], in which case
   we will set [COQCORELIB:=COQLIB].
 
@@ -96,7 +96,7 @@ val native_cmi : t -> string -> Path.t
 (** The location of the revision file *)
 val revision : t -> Path.t
 
-(** coq-core/lib directory, not sure if to keep this *)
+(** rocq-runtime/lib directory, not sure if to keep this *)
 val corelib : t -> Path.t
 
 (** coq/lib directory, not sure if to keep this *)

checker/dune

@@ -4,17 +4,29 @@
 ; duplicate module names in the whole build.
 (library
  (name coq_checklib)
- (public_name coq-core.checklib)
+ (public_name rocq-runtime.checklib)
  (synopsis "Rocq's Standalone Proof Checker")
- (modules :standard \ coqchk votour)
+ (modules :standard \ rocqchk coqchk votour)
  (wrapped true)
- (libraries coq-core.boot coq-core.kernel))
+ (libraries rocq-runtime.boot rocq-runtime.kernel))
+
+(deprecated_library_name
+ (old_public_name coq-core.checklib)
+ (new_public_name rocq-runtime.checklib))
+
+(executable
+ (name rocqchk)
+ (public_name rocqchk)
+ (modes exe byte)
+ (package rocq-runtime)
+ (modules rocqchk)
+ (flags :standard -open Coq_checklib)
+ (libraries coq_checklib))
 
 (executable
  (name coqchk)
  (public_name coqchk)
  (modes exe byte)
- ; Move to coq-checker?
  (package coq-core)
  (modules coqchk)
  (flags :standard -open Coq_checklib)
@@ -23,7 +35,7 @@
 (executable
  (name votour)
  (public_name votour)
- (package coq-core)
+ (package rocq-runtime)
  (modules votour)
  (flags :standard -open Coq_checklib)
  (libraries coq_checklib))

checker/rocqchk.ml

@@ -0,0 +1,2 @@
+
+let () = Coqchk_main.main ()

clib/dune

@@ -1,7 +1,7 @@
 (library
  (name clib)
  (synopsis "Coq's Utility Library [general purpose]")
- (public_name coq-core.clib)
+ (public_name rocq-runtime.clib)
  (wrapped false)
  (modules_without_implementation cSig)
  (modules :standard \ unicodetable_gen)
@@ -11,6 +11,10 @@
    (memprof-limits -> memprof_coq.memprof.ml))
    str unix threads))
 
+(deprecated_library_name
+ (old_public_name coq-core.clib)
+ (new_public_name rocq-runtime.clib))
+
 (executable
  (name unicodetable_gen)
  (modules unicodetable_gen))

config/dune

@@ -1,19 +1,27 @@
 (library
  (name config)
  (synopsis "Coq Configuration Variables")
- (public_name coq-core.config)
+ (public_name rocq-runtime.config)
  (modules coq_config)
  (wrapped false))
 
+(deprecated_library_name
+  (old_public_name coq-core.config)
+  (new_public_name rocq-runtime.config))
+
 (library
  (name byte_config)
  (synopsis "Coq Configuration Variables (for bytecode only)")
- (public_name coq-core.config.byte)
+ (public_name rocq-runtime.config.byte)
  (modules coq_byte_config)
  (wrapped false)
  (libraries compiler-libs.toplevel)
  (modes byte))
 
+(deprecated_library_name
+  (old_public_name coq-core.config.byte)
+  (new_public_name rocq-runtime.config.byte))
+
 (executable (name list_plugins) (modules list_plugins))
 (rule (targets plugin_list)
   (deps (source_tree %{project_root}/plugins))

coq-core.opam

@@ -1,25 +1,7 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
 version: "dev"
-synopsis: "The Coq Proof Assistant -- Core Binaries and Tools"
-description: """
-Coq is a formal proof management system. It provides
-a formal language to write mathematical definitions, executable
-algorithms and theorems together with an environment for
-semi-interactive development of machine-checked proofs.
-
-Typical applications include the certification of properties of
-programming languages (e.g. the CompCert compiler certification
-project, or the Bedrock verified low-level programming library), the
-formalization of mathematics (e.g. the full formalization of the
-Feit-Thompson theorem or homotopy type theory) and teaching.
-
-This package includes the Coq core binaries, plugins, and tools, but
-not the vernacular standard library.
-
-Note that in this setup, Coq needs to be started with the -boot and
--noinit options, as will otherwise fail to find the regular Coq
-prelude, now living in the rocq-core package."""
+synopsis: "Compatibility binaries for Coq after the Rocq renaming"
 maintainer: ["The Coq development team <[email protected]>"]
 authors: ["The Coq development team, INRIA, CNRS, and contributors"]
 license: "LGPL-2.1-only"
@@ -28,33 +10,21 @@ doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/coq/issues"
 depends: [
   "dune" {>= "3.8"}
-  "ocaml" {>= "4.09.0"}
-  "ocamlfind" {>= "1.8.1"}
-  "zarith" {>= "1.11"}
-  "conf-linux-libc-dev" {os = "linux"}
+  "rocq-runtime" {= version}
   "odoc" {with-doc}
 ]
-depopts: ["coq-native" "memprof-limits" "memtrace"]
-dev-repo: "git+https://github.com/coq/coq.git"
 build: [
   ["dune" "subst"] {dev}
-  [ "./configure"
-    "-prefix" prefix
-    "-mandir" man
-    "-libdir" "%{lib}%/coq"
-    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
-  ]
   [
     "dune"
     "build"
     "-p"
     name
     "-j"
     jobs
-    "--promote-install-files=false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}
   ]
-  ["dune" "install" "-p" name "--create-install-files" name]
 ]
+dev-repo: "git+https://github.com/coq/coq.git"

coqide-server.opam

@@ -20,7 +20,7 @@ doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/coq/issues"
 depends: [
   "dune" {>= "3.8"}
-  "coq-core" {= version}
+  "rocq-runtime" {= version}
   "odoc" {with-doc}
 ]
 build: [

coqpp/coqpp.ml

@@ -0,0 +1 @@
+let () = Coqpp_main.main (List.tl (Array.to_list Sys.argv))

coqpp/coqpp_main.ml

@@ -693,17 +693,13 @@ let pr_ast fmt = function
 | ArgumentExt arg -> fprintf fmt "%a@\n" ArgumentExt.print_ast arg
 
 let help () =
-  Format.eprintf "Usage: coqpp file.mlg@\n%!";
+  Format.eprintf "Usage: rocq preprocess-mlg file.mlg@\n%!";
   exit 1
 
-let parse () =
-  let () =
-    if Array.length Sys.argv <> 2
-    then help ()
-  in
-  match Sys.argv.(1) with
-  | "-help" | "--help" -> help ()
-  | file -> file
+let parse = function
+  | ["-help"|"--help"] -> help()
+  | [file] -> file
+  | _ -> help ()
 
 let output_name file =
   try
@@ -712,8 +708,8 @@ let output_name file =
   | Invalid_argument _ ->
     fatal "Input file must have an extension for coqpp [input.ext -> input.ml]"
 
-let () =
-  let file = parse () in
+let main args =
+  let file = parse args in
   let output = output_name file in
   let ast = parse_file file in
   let chan = open_out output in

coqpp/coqpp_main.mli

@@ -0,0 +1 @@
+val main : string list -> unit