rename package coq-core -> rocq-runtime

SkySkimmer · Dec 12, 2024 · 3d60180 · 3d60180
1 parent ed02865
commit 3d60180
Show file tree

Hide file tree

Showing 217 changed files with 962 additions and 735 deletions.
diff --git a/.github/workflows/ci-macos.yml b/.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: |

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
@@ -81,7 +81,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
@@ -232,6 +232,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/
@@ -336,7 +337,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

diff --git a/INSTALL.md b/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.
 

diff --git a/Makefile b/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 rocq-runtime.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
 #

diff --git a/boot/dune b/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))
diff --git a/boot/env.ml b/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
 

diff --git a/boot/env.mli b/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 *)

diff --git a/checker/dune b/checker/dune
@@ -4,26 +4,30 @@
 ; 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)
  (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 coqchk)
  (public_name coqchk)
  (modes exe byte)
  ; Move to coq-checker?
- (package coq-core)
+ (package rocq-runtime)
  (modules coqchk)
  (flags :standard -open Coq_checklib)
  (libraries coq_checklib))
 
 (executable
  (name votour)
  (public_name votour)
- (package coq-core)
+ (package rocq-runtime)
  (modules votour)
  (flags :standard -open Coq_checklib)
  (libraries coq_checklib))

diff --git a/clib/dune b/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))

diff --git a/config/dune b/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))

diff --git a/coq-core.opam b/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"
diff --git a/coqide-server.opam b/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: [

diff --git a/coqpp/dune b/coqpp/dune
@@ -10,6 +10,6 @@
 (executable
  (name coqpp_main)
  (public_name coqpp)
- (package coq-core)
+ (package rocq-runtime)
  (libraries coqpp)
  (modules coqpp_main))
diff --git a/default.nix b/default.nix
@@ -120,7 +120,7 @@ stdenv.mkDerivation rec {
   # From https://github.com/NixOS/nixpkgs/blob/master/pkgs/build-support/ocaml/dune.nix
   installPhase = ''
     runHook preInstall
-    dune install --prefix $out --libdir $OCAMLFIND_DESTDIR coq-core rocq-core coqide-server ${optionalString buildIde "coqide"}
+    dune install --prefix $out --libdir $OCAMLFIND_DESTDIR rocq-runtime coq-core rocq-core coqide-server ${optionalString buildIde "coqide"}
     runHook postInstall
   '';
 
@@ -131,7 +131,7 @@ stdenv.mkDerivation rec {
 
   createFindlibDestdir = !shell;
 
-  postInstall = "ln -s $out/lib/coq-core $OCAMLFIND_DESTDIR/coq-core";
+  postInstall = "ln -s $out/lib/rocq-runtime $OCAMLFIND_DESTDIR/rocq-runtime && ln -s $out/lib/coq-core $OCAMLFIND_DESTDIR/coq-core";
 
   inherit doInstallCheck;
 

diff --git a/dev/bench/bench.sh b/dev/bench/bench.sh
@@ -462,7 +462,7 @@ export PROFILING=1
 export COQ_PROFILE_COMPONENTS=command,parse_command,partac.perform
 
 # packages tied to the coq commit need to be pinned accordingly
-core_packages='coq-core rocq-core coq-stdlib coqide-server coq'
+core_packages='rocq-runtime coq-core rocq-core coq-stdlib coqide-server coq'
 
 for coq_opam_package in $core_packages $coq_opam_packages; do
 
@@ -509,7 +509,8 @@ $coq_opam_package (unknown package)"
 
         git checkout -q $COQ_HASH
 
-        if [ "$coq_opam_package" = rocq-core ] && ! [ -e $coq_opam_package.opam ]; then
+        if { [ "$coq_opam_package" = rocq-core ] || [ "$coq_opam_package" = rocq-runtime ]; } \
+             && ! [ -e $coq_opam_package.opam ]; then
           echo "Skipping $coq_opam_package for $RUNNER"
           continue 2
         fi

diff --git a/dev/bench/dune b/dev/bench/dune
@@ -21,6 +21,6 @@
 (executable
  (name timelog2html)
  (public_name coqtimelog2html)
- (package coq-core)
+ (package rocq-runtime)
  (modules timelog2html)
  (libraries benchlib))