the 'coq.color' dependency is now not needed for the concrete Minuska

h0nzZik · Jan 22, 2024 · afe4e68 · afe4e68
1 parent 8bc5558
commit afe4e68
Show file tree

Hide file tree

Showing 5 changed files with 49 additions and 3 deletions.
diff --git a/flake.nix b/flake.nix
@@ -14,7 +14,6 @@
 
       in {
 
-        # The 'matching logic in Coq' library
         packages.minuska
         = coqPackages.callPackage 
         ( { coq, stdenv }:
@@ -26,7 +25,6 @@
             coq
             coqPackages.equations
             coqPackages.stdpp
-            coqPackages.CoLoR
             coq.ocaml
             coq.ocamlPackages.zarith
           ];
@@ -36,6 +34,22 @@
           passthru = { inherit coqPackages; };
         } ) { } ;
 
+        packages.minuska-symbolic
+        = coqPackages.callPackage 
+        ( { coq, stdenv }:
+        stdenv.mkDerivation {
+          name = "minuska-symbolic";
+          src = ./minuska-symbolic;
+
+          propagatedBuildInputs = [
+            self.outputs.packages.${system}.minuska
+            coqPackages.CoLoR
+          ];
+          enableParallelBuilding = true;
+          installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
+
+          passthru = { inherit coqPackages; };
+        } ) { } ;
 
         packages.default = self.outputs.packages.${system}.minuska;
 
@@ -48,6 +62,16 @@
                 inputsFrom = [minuska];
                 packages = [minuska.coqPackages.coq-lsp minuska.coqPackages.coqide];
               };
+
+          minuska-symbolic =
+            let
+              minuska-symbolic = self.outputs.packages.${system}.minuska-symbolic;
+            in
+              pkgs.mkShell {
+                inputsFrom = [minuska-symbolic];
+                packages = [minuska-symbolic.coqPackages.coq-lsp minuska-symbolic.coqPackages.coqide];
+              };
+
         };
       }
     )

diff --git a/minuska-symbolic/Makefile b/minuska-symbolic/Makefile
@@ -0,0 +1,19 @@
+all: Makefile.coq
+	@+$(MAKE) -f Makefile.coq all
+
+install: Makefile.coq
+	@+$(MAKE) -f Makefile.coq install
+
+clean: Makefile.coq
+	@+$(MAKE) -f Makefile.coq cleanall
+	@rm -f Makefile.coq Makefile.coq.conf
+
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
+
+force _CoqProject Makefile: ;
+
+%: Makefile.coq force
+	@+$(MAKE) -f Makefile.coq $@
+
+.PHONY: all clean force install
diff --git a/minuska-symbolic/_CoqProject b/minuska-symbolic/_CoqProject
@@ -0,0 +1,4 @@
+-R theories MinuskaSymbolic
+
+theories/color.v
+
diff --git a/minuska/theories/color.v → minuska-symbolic/theories/color.v b/minuska/theories/color.v → minuska-symbolic/theories/color.v
diff --git a/minuska/_CoqProject b/minuska/_CoqProject
@@ -13,7 +13,6 @@ theories/minuska.v
 theories/string_variables.v
 theories/BuiltinValue.v
 theories/builtins.v
-theories/color.v
 theories/basic_matching.v
 theories/try_match.v
 theories/naive_interpreter.v