From 4264aec518d5407f345c58e18e014e15e9ae96af Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 5 Jan 2021 11:34:35 +0100
Subject: [sysinit] new component for system initialization

This component holds the code for initializing Coq:
- parsing arguments not specific to the toplevel
- initializing all components from vernac downwards (no stm)

This commit moves stm specific arguments parsing to stm/stmargs.ml
---
 dev/base_include           | 1 -
 dev/dune                   | 1 +
 dev/tools/update-compat.py | 2 +-
 3 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/base_include b/dev/base_include
index daee2d97c5..f375a867bc 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -134,7 +134,6 @@ open ComDefinition
 open Indschemes
 open Ind_tables
 open Auto_ind_decl
-open Coqinit
 open Coqtop
 open Himsg
 open Metasyntax
diff --git a/dev/dune b/dev/dune
index a6d88c94d2..ae801f9e83 100644
--- a/dev/dune
+++ b/dev/dune
@@ -34,6 +34,7 @@
     %{lib:coq.tactics:tactics.cma}
     %{lib:coq.vernac:vernac.cma}
     %{lib:coq.stm:stm.cma}
+    %{lib:coq.sysinit:sysinit.cma}
     %{lib:coq.toplevel:toplevel.cma}
     %{lib:coq.plugins.ltac:ltac_plugin.cma}
     %{lib:coq.top_printers:top_printers.cmi}
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
index 666fb6cc91..a14b98c73c 100755
--- a/dev/tools/update-compat.py
+++ b/dev/tools/update-compat.py
@@ -64,7 +64,7 @@ DEFAULT_NUMBER_OF_OLD_VERSIONS = 2
 RELEASE_NUMBER_OF_OLD_VERSIONS = 2
 MASTER_NUMBER_OF_OLD_VERSIONS = 3
 EXTRA_HEADER = '\n(** Compatibility file for making Coq act similar to Coq v%s *)\n'
-COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml')
+COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'sysinit', 'coqargs.ml')
 DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template')
 TEST_SUITE_RUN_PATH = os.path.join(ROOT_PATH, 'test-suite', 'tools', 'update-compat', 'run.sh')
 TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i)
-- 
cgit v1.2.3


From be070cfb10a59be13a478a7efbf92dd3e22401ed Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 27 Jan 2021 11:35:35 +0100
Subject: Add sysinit to load_printer lists

---
 dev/core.dbg           | 1 +
 dev/core_dune.dbg      | 1 +
 dev/dune_db_408        | 1 +
 dev/dune_db_409        | 1 +
 dev/ocamldebug-coq.run | 2 +-
 5 files changed, 5 insertions(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/core.dbg b/dev/core.dbg
index 6d52bae773..dcf9910b0b 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -16,5 +16,6 @@ load_printer parsing.cma
 load_printer printing.cma
 load_printer tactics.cma
 load_printer vernac.cma
+load_printer sysinit.cma
 load_printer stm.cma
 load_printer toplevel.cma
diff --git a/dev/core_dune.dbg b/dev/core_dune.dbg
index 3f73cf126a..da3022644d 100644
--- a/dev/core_dune.dbg
+++ b/dev/core_dune.dbg
@@ -17,5 +17,6 @@ load_printer parsing.cma
 load_printer printing.cma
 load_printer tactics.cma
 load_printer vernac.cma
+load_printer sysinit.cma
 load_printer stm.cma
 load_printer toplevel.cma
diff --git a/dev/dune_db_408 b/dev/dune_db_408
index 5f826fe383..bc86020d56 100644
--- a/dev/dune_db_408
+++ b/dev/dune_db_408
@@ -17,6 +17,7 @@ load_printer parsing.cma
 load_printer printing.cma
 load_printer tactics.cma
 load_printer vernac.cma
+load_printer sysinit.cma
 load_printer stm.cma
 load_printer toplevel.cma
 
diff --git a/dev/dune_db_409 b/dev/dune_db_409
index 2e58272c75..adb1f76872 100644
--- a/dev/dune_db_409
+++ b/dev/dune_db_409
@@ -16,6 +16,7 @@ load_printer parsing.cma
 load_printer printing.cma
 load_printer tactics.cma
 load_printer vernac.cma
+load_printer sysinit.cma
 load_printer stm.cma
 load_printer toplevel.cma
 
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 534f20f85b..db15d9705a 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -19,7 +19,7 @@ exec $OCAMLDEBUG \
     -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
     -I $COQTOP/gramlib/.pack \
     -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
-    -I $COQTOP/library -I $COQTOP/engine \
+    -I $COQTOP/library -I $COQTOP/engine -I $COQTOP/sysinit \
     -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
     -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
     -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \
-- 
cgit v1.2.3