First working prototype of the library

AgdaUnusedOpens/AgdaCompiler.fs

@@ -1,5 +1,6 @@
 namespace AgdaUnusedOpens
 
+open System.Diagnostics
 open System.IO
 
 type AgdaCompiler =
@@ -12,12 +13,28 @@ type AgdaCompiler =
 [<RequireQualifiedAccess>]
 module AgdaCompiler =
 
+    let private compile (config : AgdaCompiler) (f : AgdaFile) : int =
+        use proc = new Process ()
+        proc.StartInfo.FileName <- config.Compiler.FullName
+        proc.StartInfo.Arguments <- sprintf "%s" (Path.combine config.AgdaRoot f.Path).FullName
+        proc.StartInfo.WorkingDirectory <- config.AgdaRoot.FullName
+        proc.StartInfo.UseShellExecute <- false
+        proc.StartInfo.RedirectStandardOutput <- true
+        proc.StartInfo.RedirectStandardError <- true
+        if proc.Start () then
+            proc.StandardOutput.ReadToEnd () |> ignore
+            proc.StandardError.ReadToEnd () |> ignore
+            proc.WaitForExit ()
+        proc.ExitCode
+
     let compiles (config : AgdaCompiler) (f : AgdaFile) : bool =
-        // Write it out with a different, temporary name, and then run the compiler.
-        // Delete the temporary file afterwards.
-        let tempName = failwith ""
+        // Write it out with a temporary name
+        let tempName = "temporaryModuleName"
         let newFile = AgdaFile.rename tempName f
         AgdaFile.flush config.AgdaRoot newFile
-        // run the compiler
+
+        let exitCode = compile config newFile
+
+        // Delete the temporary file
         (Path.combine config.AgdaRoot newFile.Path).Delete()
-        true
+        exitCode = 0

AgdaUnusedOpens/AgdaFile.fs

@@ -21,6 +21,7 @@ module Path =
     let combine (agdaRoot : DirectoryInfo) (p : Path) : FileInfo =
         p
         |> fold (fun soFar next -> Path.Combine (soFar, next)) agdaRoot.FullName
+        |> sprintf "%s.agda"
         |> FileInfo
 
     let rename (newModule : string) (p : Path) =

AgdaUnusedOpens/Graph.fs

@@ -71,6 +71,7 @@ module Graph =
         proc.StartInfo.Arguments <- sprintf "%s --dependency-graph=%s" (Path.combine agda.AgdaRoot f.Path).FullName tmp
         let res = proc.Start ()
         assert (res = true)
+        proc.WaitForExit ()
         tmp
         |> File.ReadAllText
         |> parse