fix examples

MetaCoq · Jan 13, 2023 · d501960 · d501960
1 parent 3f170f1
commit d501960
Show file tree

Hide file tree

Showing 11 changed files with 31 additions and 21 deletions.
diff --git a/Makefile b/Makefile
@@ -148,10 +148,10 @@ erasure: safechecker
 erasure-plugin: erasure template-pcuic
 	$(MAKE) -C safechecker-plugin
 
-examples: safechecker erasure
+examples: safechecker-plugin erasure-plugin
 	$(MAKE) -C examples
 
-test-suite: template-coq safechecker erasure
+test-suite: safechecker-plugin erasure-plugin
 	$(MAKE) -C test-suite
 
 translations: template-coq

diff --git a/configure.sh b/configure.sh
@@ -26,8 +26,8 @@ then
         ERASURE_DEPS="-R ../safechecker/theories MetaCoq.SafeChecker"
         ERASURE_PLUGIN_DEPS="-R ../template-pcuic/theories MetaCoq.TemplatePCUIC -R ../erasure/theories MetaCoq.Erasure  -I ../template-coq"
         TRANSLATIONS_DEPS="-R ../template-coq/theories MetaCoq.Template -I ../template-coq"
-        EXAMPLES_DEPS="-R ../erasure/theories MetaCoq.Erasure"
-        TEST_SUITE_DEPS="-R ../erasure/theories MetaCoq.Erasure"
+        EXAMPLES_DEPS="-R ../safechecker-plugin/theories MetaCoq.SafecheckerPlugin -R ../erasure-plugin/theories MetaCoq.ErasurePlugin"
+        TEST_SUITE_DEPS="-R ../safechecker-plugin/theories MetaCoq.SafecheckerPlugin -R ../erasure-plugin/theories MetaCoq.ErasurePlugin"
         PLUGIN_DEMO_DEPS="-R ../../template-coq/theories MetaCoq.Template -I ../../template-coq/"
         echo "METACOQ_CONFIG = local" > Makefile.conf
     else
@@ -69,8 +69,8 @@ then
     echo ${COMMON_DEPS} ${PCUIC_DEPS} ${SAFECHECKER_DEPS} ${ERASURE_DEPS} >> erasure/metacoq-config
     echo ${COMMON_DEPS} ${PCUIC_DEPS} ${ERASURE_DEPS} ${TEMPLATE_PCUIC_DEPS} ${ERASURE_PLUGIN_DEPS} >> erasure-plugin/metacoq-config
     echo ${COMMON_DEPS} ${PCUIC_DEPS} ${TRANSLATIONS_DEPS} >> translations/metacoq-config
-    echo ${COMMON_DEPS} ${PCUIC_DEPS} ${SAFECHECKER_DEPS} ${TEMPLATE_PCUIC_DEPS} ${ERASURE_DEPS} ${TRANSLATIONS_DEPS} ${EXAMPLES_DEPS} >> examples/metacoq-config
-    echo ${COMMON_DEPS} ${PCUIC_DEPS} ${SAFECHECKER_DEPS} ${TEMPLATE_PCUIC_DEPS} ${ERASURE_DEPS} ${TRANSLATIONS_DEPS} ${TEST_SUITE_DEPS} >> test-suite/metacoq-config
+    echo ${COMMON_DEPS} ${PCUIC_DEPS} ${SAFECHECKER_DEPS} ${TEMPLATE_PCUIC_DEPS} ${ERASURE_DEPS} ${TRANSLATIONS_DEPS} ${ERASURE_PLUGIN_DEPS} ${EXAMPLES_DEPS} >> examples/metacoq-config
+    echo ${COMMON_DEPS} ${PCUIC_DEPS} ${SAFECHECKER_DEPS} ${TEMPLATE_PCUIC_DEPS} ${ERASURE_DEPS} ${TRANSLATIONS_DEPS} ${ERASURE_PLUGIN_DEPS} ${TEST_SUITE_DEPS} >> test-suite/metacoq-config
     echo ${PLUGIN_DEMO_DEPS} >> test-suite/plugin-demo/metacoq-config
 
 else

diff --git a/erasure-plugin/_PluginProject.in b/erasure-plugin/_PluginProject.in
@@ -1,6 +1,6 @@
 -I src
--Q src MetaCoq.Erasure
--R theories MetaCoq.Erasure
+-Q src MetaCoq.ErasurePlugin
+-R theories MetaCoq.ErasurePlugin
 src/META.coq-metacoq-erasure
 
 src/ssrbool.ml

diff --git a/erasure-plugin/clean_extraction.sh b/erasure-plugin/clean_extraction.sh
@@ -11,8 +11,8 @@ shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
 
 files=`cat ../template-coq/_PluginProject | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
 
-if [[ ! -f "src/metacoq_safechecker_plugin.cmxs" ||
-           "src/metacoq_safechecker_plugin.cmxs" -ot "theories/Extraction.vo" ]]
+if [[ ! -f "src/metacoq_erasure_plugin.cmxs" ||
+           "src/metacoq_erasure_plugin.cmxs" -ot "theories/Extraction.vo" ]]
 then
     cd src
     # Move extracted modules to build the certicoq compiler plugin

diff --git a/examples/add_constructor.v b/examples/add_constructor.v
@@ -1,5 +1,6 @@
 (* Distributed under the terms of the MIT license. *)
-From MetaCoq.Template Require Import utils All.
+From MetaCoq.Utils Require Import utils.
+From MetaCoq.Template Require Import All.
 
 Import MCMonadNotation.
 

diff --git a/examples/demo.v b/examples/demo.v
@@ -1,5 +1,6 @@
 (* Distributed under the terms of the MIT license. *)
-From MetaCoq.Template Require Import utils All.
+From MetaCoq.Utils Require Import utils.
+From MetaCoq.Template Require Import All.
 
 Import MCMonadNotation.
 

diff --git a/examples/metacoq_tour.v b/examples/metacoq_tour.v
@@ -1,4 +1,6 @@
-From MetaCoq.Template Require config utils All.
+From MetaCoq.Utils Require Import utils.
+From MetaCoq.Common Require Import config.
+From MetaCoq.Template Require Import All.
 From MetaCoq.Template Require Import TemplateMonad.
 From MetaCoq.PCUIC Require Import PCUICAst PCUICReduction PCUICCumulativity PCUICTyping PCUICSafeLemmata.
 
@@ -58,7 +60,8 @@ Check PCUICSR.subject_reduction.
 
 (** Verified conversion and type-checking *)
 
-From MetaCoq.SafeChecker Require Import PCUICErrors PCUICWfEnv PCUICWfEnvImpl PCUICTypeChecker PCUICSafeChecker PCUICSafeRetyping Loader.
+From MetaCoq.SafeChecker Require Import PCUICErrors PCUICWfEnv PCUICWfEnvImpl PCUICTypeChecker PCUICSafeChecker PCUICSafeRetyping.
+From MetaCoq.SafecheckerPlugin Require Import Loader.
 Check PCUICSafeConversion.isconv_term_sound.
 Check PCUICSafeConversion.isconv_term_complete.
 
@@ -92,7 +95,7 @@ Qed. *)
 (* MetaCoq SafeCheck (fun x : nat => x + 1). *)
 
 (** Erasure *)
-From MetaCoq.Erasure Require Import Erasure Loader.
+From MetaCoq.ErasurePlugin Require Import Erasure Loader.
 
 (** Running erasure live in Coq *)
 Definition test (p : Ast.Env.program) : string :=

diff --git a/examples/metacoq_tour_prelude.v b/examples/metacoq_tour_prelude.v
@@ -1,5 +1,7 @@
 (* Distributed under the terms of the MIT license. *)
-From MetaCoq.Template Require Import config Universes Loader.
+From MetaCoq.Utils Require Import utils.
+From MetaCoq.Common Require Import config Universes.
+From MetaCoq.Template Require Import Loader.
 From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTyping PCUICSN PCUICLiftSubst.
 From MetaCoq.SafeChecker Require Import PCUICErrors PCUICWfEnv PCUICWfEnvImpl PCUICTypeChecker PCUICSafeChecker.
 From Equations Require Import Equations.

diff --git a/examples/tauto.v b/examples/tauto.v
@@ -1,5 +1,6 @@
 (* Distributed under the terms of the MIT license. *)
-From MetaCoq.Template Require Import utils All.
+From MetaCoq.Utils Require Import utils.
+From MetaCoq.Template Require Import All.
 
 From Equations Require Import Equations.
 

diff --git a/examples/typing_correctness.v b/examples/typing_correctness.v
@@ -64,7 +64,9 @@ Proof.
 Defined.
 *)
 (* Distributed under the terms of the MIT license. *)
-From MetaCoq.Template Require Import config Universes Loader.
+From MetaCoq.Utils Require Import utils.
+From MetaCoq.Common Require Import config Universes.
+From MetaCoq.Template Require Import Loader.
 From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTyping PCUICLiftSubst.
 From MetaCoq.SafeChecker Require Import PCUICErrors PCUICWfEnv PCUICWfEnvImpl PCUICTypeChecker PCUICSafeChecker.
 From Equations Require Import Equations.

diff --git a/safechecker-plugin/_PluginProject.in b/safechecker-plugin/_PluginProject.in
@@ -1,7 +1,7 @@
-src/META.coq-metacoq-templatepcuic
+src/META.coq-metacoq-safecheckerplugin
 -I src
--Q src MetaCoq.TemplatePCUIC
--R theories MetaCoq.TemplatePCUIC
+-Q src MetaCoq.SafecheckerPlugin
+-R theories MetaCoq.SafecheckerPlugin
 
 # src/classes0.mli
 # src/classes0.ml