Merge pull request 'fix(frontend): Tomograph compilation' (#235) from frontend/tomograph into dev

Reviewed-on: #235

Tomograph.lean

@@ -14,14 +14,14 @@ def dissect (args : List String) : IO UInt32 := do
   let fileName :: _args := args | fail s!"Must supply a file name"
   let file ← IO.FS.readFile fileName
   let (context, state) ← do Frontend.createContextStateFromFile file fileName (env? := .none) {}
-  let frontendM: Elab.Frontend.FrontendM _ :=
+  let frontendM: Frontend.FrontendM _ :=
     Frontend.mapCompilationSteps λ step => do
       IO.println s!"🐈 {step.stx.getKind.toString}"
       for (tree, i) in step.trees.zipIdx do
         IO.println s!"🌲[{i}] {← tree.toString}"
       for (msg, i) in step.msgs.zipIdx do
         IO.println s!"🔈[{i}] {← msg.toString}"
-  let (_, _) ← frontendM.run context |>.run state
+  let (_, _) ← frontendM.run {} |>.run context |>.run state
   return 0
 
 end Pantograph

flake.lock

@@ -5,11 +5,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1749398372,
+        "lastModified": 1751413152,
-        "narHash": "sha256-tYBdgS56eXYaWVW3fsnPQ/nFlgWi/Z2Ymhyu21zVM98=",
+        "narHash": "sha256-Tyw1RjYEsp5scoigs1384gIg6e0GoBVjms4aXFfRssQ=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "9305fe4e5c2a6fcf5ba6a3ff155720fbe4076569",
+        "rev": "77826244401ea9de6e3bac47c2db46005e1f30b5",
         "type": "github"
       },
       "original": {
@@ -42,11 +42,11 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1750369222,
+        "lastModified": 1751390929,
-        "narHash": "sha256-KFFTVbciXUaHgeGN1yiaUtY88OLGU0gElXx5SfICDKg=",
+        "narHash": "sha256-Wl2miy8PhNF6ue3R1ssQbsVK3foJ37tYtznNq/i14YM=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "015ecd25206734d582a1b15dd11eb10be35ca555",
+        "rev": "68a07e4af5e2e56276056b172e046a2276d21aee",
         "type": "github"
       },
       "original": {
@@ -73,11 +73,11 @@
     },
     "nixpkgs-lib": {
       "locked": {
-        "lastModified": 1748740939,
+        "lastModified": 1751159883,
-        "narHash": "sha256-rQaysilft1aVMwF14xIdGS3sj1yHlI6oKQNBRTF40cc=",
+        "narHash": "sha256-urW/Ylk9FIfvXfliA1ywh75yszAbiTEVgpPeinFyVZo=",
         "owner": "nix-community",
         "repo": "nixpkgs.lib",
-        "rev": "656a64127e9d791a334452c6b6606d17539476e2",
+        "rev": "14a40a1d7fb9afa4739275ac642ed7301a9ba1ab",
         "type": "github"
       },
       "original": {
@@ -100,16 +100,16 @@
     },
     "nixpkgs_2": {
       "locked": {
-        "lastModified": 1751048012,
+        "lastModified": 1751943650,
-        "narHash": "sha256-MYbotu4UjWpTsq01wglhN5xDRfZYLFtNk7SBY0BcjkU=",
+        "narHash": "sha256-7orTnNqkGGru8Je6Un6mq1T8YVVU/O5kyW4+f9C1mZQ=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "a684c58d46ebbede49f280b653b9e56100aa3877",
+        "rev": "88983d4b665fb491861005137ce2b11a9f89f203",
         "type": "github"
       },
       "original": {
         "owner": "nixos",
-        "ref": "nixos-24.11",
+        "ref": "nixos-25.05",
         "repo": "nixpkgs",
         "type": "github"
       }

flake.nix

@@ -2,7 +2,7 @@
   description = "Pantograph";
 
   inputs = {
-    nixpkgs.url = "github:nixos/nixpkgs/nixos-24.11";
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-25.05";
     flake-parts.url = "github:hercules-ci/flake-parts";
     lean4-nix.url = "github:lenianiva/lean4-nix";
   };
@@ -45,10 +45,6 @@
           ./Pantograph.lean
           (fileFilter (file: file.hasExt "lean") ./Pantograph)
         ];
-        set-repl = unions [
-          ./Main.lean
-          ./Repl.lean
-        ];
         set-test = unions [
           (fileFilter (file: file.hasExt "lean") ./Test)
         ];
@@ -62,14 +58,22 @@
           root = src;
           fileset = unions [
             set-project
-            set-repl
+            ./Main.lean
+            ./Repl.lean
+          ];
+        };
+        src-tomograph = toSource {
+          root = src;
+          fileset = unions [
+            set-project
+            ./Tomograph.lean
           ];
         };
         src-test = toSource {
           root = src;
           fileset = unions [
             set-project
-            set-repl
+            ./Repl.lean
             set-test
           ];
         };
@@ -84,6 +88,12 @@
           deps = [project];
           src = src-repl;
         };
+        tomograph = pkgs.lean.buildLeanPackage {
+          name = "tomograph";
+          roots = ["Tomograph"];
+          deps = [project];
+          src = src-tomograph;
+        };
         test = pkgs.lean.buildLeanPackage {
           name = "Test";
           # NOTE: The src directory must be ./. since that is where the import
@@ -98,6 +108,7 @@
           inherit (pkgs.lean) lean lean-all;
           inherit (project) sharedLib iTree;
           inherit (repl) executable;
+          tomograph = tomograph.executable;
           default = repl.executable;
         };
         legacyPackages = {

lakefile.lean

@@ -18,7 +18,6 @@ lean_exe repl {
   supportInterpreter := true
 }
 
-@[default_target]
 lean_exe tomograph {
   root := `Tomograph
   -- Solves the native symbol not found problem