Merge pull request #829 from MetaCoq/add-utils-and-common-initial-folders

Add utils and common initial folders and reorganize code and plugins

Author: tabareau

.github/workflows/nix-action-coq-8.16-macos.yml

@@ -118,6 +118,14 @@ jobs:
       name: 'Building/fetching previous CI target: equations'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
         --argstr job "equations"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-utils'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
+        --argstr job "metacoq-utils"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-common'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
+        --argstr job "metacoq-common"
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: metacoq-template-coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
@@ -134,6 +142,18 @@ jobs:
       name: 'Building/fetching previous CI target: metacoq-erasure'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
         --argstr job "metacoq-erasure"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-template-pcuic'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
+        --argstr job "metacoq-template-pcuic"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-safechecker-plugin'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
+        --argstr job "metacoq-safechecker-plugin"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-erasure-plugin'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
+        --argstr job "metacoq-erasure-plugin"
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"

.github/workflows/nix-action-coq-8.16-ubuntu.yml

@@ -118,6 +118,14 @@ jobs:
       name: 'Building/fetching previous CI target: equations'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
         --argstr job "equations"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-utils'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
+        --argstr job "metacoq-utils"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-common'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
+        --argstr job "metacoq-common"
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: metacoq-template-coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
@@ -134,6 +142,18 @@ jobs:
       name: 'Building/fetching previous CI target: metacoq-erasure'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
         --argstr job "metacoq-erasure"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-template-pcuic'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
+        --argstr job "metacoq-template-pcuic"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-safechecker-plugin'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
+        --argstr job "metacoq-safechecker-plugin"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-erasure-plugin'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
+        --argstr job "metacoq-erasure-plugin"
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"

.gitignore

@@ -233,6 +233,8 @@ checker/src/wf.mli
 /pcuic/src/classes0.mli
 /pcuic/src/classes0.ml
 /checker/metacoq-config
+/template-coq/metacoq-config
+/common/metacoq-config
 /translations/metacoq-config
 /erasure/_CoqProject
 /erasure/_PluginProject
@@ -244,6 +246,8 @@ checker/src/wf.mli
 /safechecker/metacoq-config
 /safechecker/_PluginProject
 /safechecker/_CoqProject
+/template-coq/_CoqProject
+/common/_CoqProject
 /safechecker/Makefile.safechecker.conf
 /safechecker/Makefile.safechecker
 /safechecker/Makefile.plugin.conf
@@ -289,6 +293,7 @@ test-suite/myMain.mli
 test-suite/myMain.ml
 test-suite/plugin-demo/Makefile.plugin
 
+
 template-coq/Makefile.plugin-e
 template-coq/Makefile.template-e
 template-coq/src/g_template_coq.ml
@@ -365,3 +370,30 @@ test-suite/plugin-demo/metacoq-config
 erasure/META
 safechecker/META
 template-coq/META
+
+
+template-pcuic/demo.v
+template-pcuic/Makefile.local
+template-pcuic/_CoqProject
+template-pcuic/Makefile.templatepcuic
+template-pcuic/Makefile.templatepcuic.conf
+
+safechecker-plugin/metacoq-config
+safechecker-plugin/demo.v
+safechecker-plugin/Makefile.local
+safechecker-plugin/_CoqProject
+safechecker-plugin/_PluginProject
+safechecker-plugin/Makefile.safecheckerplugin
+safechecker-plugin/Makefile.safecheckerplugin.conf
+safechecker-plugin/Makefile.plugin
+safechecker-plugin/Makefile.plugin.conf
+
+erasure-plugin/metacoq-config
+erasure-plugin/demo.v
+erasure-plugin/Makefile.local
+erasure-plugin/_CoqProject
+erasure-plugin/_PluginProject
+erasure-plugin/Makefile.erasureplugin
+erasure-plugin/Makefile.erasureplugin.conf
+erasure-plugin/Makefile.plugin
+erasure-plugin/Makefile.plugin.conf

.nix/cachedMake.sh

@@ -43,10 +43,13 @@ my-cachedMake (){
     fi
 }
 
+my-cachedMake 'utils' 'utils/theories' 'MetaCoq.Utils'
+my-cachedMake 'common' 'common/theories' 'MetaCoq.Common'
 my-cachedMake 'template-coq' 'template-coq/theories' 'MetaCoq.Template'
 my-cachedMake 'pcuic' 'pcuic/theories' 'MetaCoq.PCUIC'
 my-cachedMake 'safechecker' 'safechecker/theories' 'MetaCoq.SafeChecker'
 my-cachedMake 'erasure' 'erasure/theories' 'MetaCoq.Erasure'
+my-cachedMake 'template-pcuic' 'template-pcuic/theories' 'MetaCoq.TemplatePCUIC'
 
 unset -f my-nix-build-with-target
 unset -f my-cachedMake

.nix/coq-overlays/metacoq/default.nix

@@ -25,7 +25,7 @@ let
   releaseRev = v: "v${v}";
 
   # list of core metacoq packages sorted by dependency order
-  packages = [ "template-coq" "pcuic" "safechecker" "erasure" "all" ];
+  packages = [ "utils" "common" "template-coq" "pcuic" "safechecker" "erasure" "template-pcuic" "safechecker-plugin" "erasure-plugin" "all" ];
 
   template-coq = metacoq_ "template-coq";
 
@@ -49,16 +49,15 @@ let
           patchShebangs ./configure.sh
           patchShebangs ./template-coq/update_plugin.sh
           patchShebangs ./template-coq/gen-src/to-lower.sh
-          patchShebangs ./pcuic/clean_extraction.sh
-          patchShebangs ./safechecker/clean_extraction.sh
-          patchShebangs ./erasure/clean_extraction.sh
+          patchShebangs ./safechecker-plugin/clean_extraction.sh
+          patchShebangs ./erasure-plugin/clean_extraction.sh
           echo "CAMLFLAGS+=-w -60 # Unused module" >> ./safechecker/Makefile.plugin.local
-          sed -i -e 's/mv $i $newi;/mv $i tmp; mv tmp $newi;/' ./template-coq/gen-src/to-lower.sh ./pcuic/clean_extraction.sh ./safechecker/clean_extraction.sh ./erasure/clean_extraction.sh
+          sed -i -e 's/mv $i $newi;/mv $i tmp; mv tmp $newi;/' ./template-coq/gen-src/to-lower.sh ./safechecker-plugin/clean_extraction.sh ./erasure-plugin/clean_extraction.sh
         '' ;
 
         configurePhase = optionalString (package == "all") pkgallMake + ''
           touch ${pkgpath}/metacoq-config
-        '' + optionalString (elem package ["safechecker" "erasure"]) ''
+        '' + optionalString (elem package ["safechecker" "erasure" "template-pcuic" "safechecker-plugin" "erasure-plugin"]) ''
           echo  "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config
         '' + optionalString (package == "single") ''
           ./configure.sh local

Makefile

@@ -12,7 +12,7 @@ ifeq '$(METACOQ_CONFIG)' 'local'
   export OCAMLPATH
 endif
 
-.PHONY: printconf all template-coq pcuic erasure install uninstall html clean mrproper .merlin test-suite translations
+.PHONY: printconf all utils template-coq pcuic erasure install uninstall html clean mrproper .merlin test-suite translations
 
 printconf:
 ifeq '$(METACOQ_CONFIG)' 'local'
@@ -27,92 +27,139 @@ endif
 endif
 
 install: all translations
+	$(MAKE) -C utils install
+	$(MAKE) -C common install
 	$(MAKE) -C template-coq install
 	$(MAKE) -C pcuic install
 	$(MAKE) -C safechecker install
+	$(MAKE) -C template-pcuic install
+	$(MAKE) -C safechecker-plugin install
 	$(MAKE) -C erasure install
 	$(MAKE) -C translations install
 
 uninstall:
+	$(MAKE) -C utils uninstall
+	$(MAKE) -C common uninstall
 	$(MAKE) -C template-coq uninstall
 	$(MAKE) -C pcuic uninstall
 	$(MAKE) -C safechecker uninstall
+	$(MAKE) -C template-pcuic uninstall
+	$(MAKE) -C safechecker-plugin uninstall
 	$(MAKE) -C erasure uninstall
 	$(MAKE) -C translations uninstall
 
 html: all
 	"coqdoc" --multi-index -toc -utf8 -html \
     --with-header ./html/resources/header.html --with-footer ./html/resources/footer.html \
+		-R utils/theories MetaCoq.Utils \
+		-R common/theories MetaCoq.Common \
 		-R template-coq/theories MetaCoq.Template \
 		-R pcuic/theories MetaCoq.PCUIC \
 		-R safechecker/theories MetaCoq.SafeChecker \
+		-R template-pcuic/theories MetaCoq.TemplatePCUIC \
 		-R erasure/theories MetaCoq.Erasure \
+		-R erasure-plugin/theories MetaCoq.ErasurePlugin \
 		-R translations MetaCoq.Translations \
 		-R examples MetaCoq.Examples \
 		-d html */theories/*.v */theories/*/*.v translations/*.v examples/*.v
 
 clean:
+	$(MAKE) -C utils clean
+	$(MAKE) -C common clean
 	$(MAKE) -C template-coq clean
 	$(MAKE) -C pcuic clean
 	$(MAKE) -C safechecker clean
+	$(MAKE) -C template-pcuic clean
 	$(MAKE) -C erasure clean
+	$(MAKE) -C erasure-plugin clean
 	$(MAKE) -C examples clean
 	$(MAKE) -C test-suite clean
 	$(MAKE) -C translations clean
 
 vos:
+	$(MAKE) -C utils
+	$(MAKE) -C common
 	$(MAKE) -C template-coq
 	$(MAKE) -C pcuic vos
 	$(MAKE) -C safechecker vos
+	$(MAKE) -C template-pcuic vos
 	$(MAKE) -C erasure vos
+	$(MAKE) -C erasure-plugin vos
 	$(MAKE) -C translations vos
 
 quick:
+	$(MAKE) -C utils
+	$(MAKE) -C common
 	$(MAKE) -C template-coq
 	$(MAKE) -C pcuic quick 
 	$(MAKE) -C safechecker quick
+	$(MAKE) -C template-pcuic quick 
 	$(MAKE) -C erasure quick
+	$(MAKE) -C erasure-plugin quick
 	$(MAKE) -C translations quick
 
 mrproper:
+	$(MAKE) -C utils mrproper
+	$(MAKE) -C common mrproper
 	$(MAKE) -C template-coq mrproper
 	$(MAKE) -C pcuic mrproper
 	$(MAKE) -C safechecker mrproper
+	$(MAKE) -C template-pcuic mrproper
 	$(MAKE) -C erasure mrproper
+	$(MAKE) -C erasure-plugin mrproper
 	$(MAKE) -C examples mrproper
 	$(MAKE) -C test-suite mrproper
 	$(MAKE) -C translations mrproper
 
 .merlin:
+	$(MAKE) -C utils .merlin
+	$(MAKE) -C common .merlin
 	$(MAKE) -C template-coq .merlin
 	$(MAKE) -C pcuic .merlin
 	$(MAKE) -C safechecker .merlin
+	$(MAKE) -C template-pcuic .merlin
 	$(MAKE) -C erasure .merlin
+	$(MAKE) -C erasure-plugin .merin
 
-template-coq:
+utils:
+	$(MAKE) -C utils
+
+common: utils
+	$(MAKE) -C common
+
+template-coq: common
 	$(MAKE) -C template-coq
 
-pcuic: template-coq
+pcuic: common
 	$(MAKE) -C pcuic
 
-safechecker: template-coq pcuic
+safechecker: pcuic
 	$(MAKE) -C safechecker
 
-erasure: template-coq safechecker pcuic
+template-pcuic: template-coq pcuic
+	$(MAKE) -C template-pcuic
+
+safechecker-plugin: safechecker template-pcuic
+	$(MAKE) -C safechecker-plugin
+
+erasure: safechecker
 	$(MAKE) -C erasure
 
-examples: safechecker erasure
+erasure-plugin: erasure template-pcuic
+	$(MAKE) -C erasure-plugin
+
+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
 	$(MAKE) -C translations
 
 cleanplugins:
 	$(MAKE) -C template-coq cleanplugin
-	$(MAKE) -C safechecker cleanplugin
+	$(MAKE) -C safechecker-plugin cleanplugin
 	$(MAKE) -C erasure cleanplugin
 
 ci-local-noclean:

build-packages.sh

@@ -1,6 +1,6 @@
 #!/bin/bash
 
-if [[ $(git grep -c todo | grep theories) = template-coq/theories/utils/MCUtils.v:3 ]]
+if [[ $(git grep -c todo | grep theories) = utils/theories/MCUtils.v:3 ]]
 then
     echo "No todos found"
     if [[ $(git grep -c Admitted | grep theories) = "" ]]
@@ -14,7 +14,7 @@ then
     fi
 else
     echo "Found todos:"
-    git grep -c todo | grep theories | grep -v "template-coq/theories/utils/MCUtils.v:3"
+    git grep -c todo | grep theories | grep -v "utils/theories/MCUtils.v:3"
     exit 1
 fi
 endef