Skip to content

Commit

Permalink
adopt Mario's solution for the paths
Browse files Browse the repository at this point in the history
  • Loading branch information
javra committed Jan 2, 2024
1 parent 90ce9d5 commit d391197
Showing 1 changed file with 8 additions and 21 deletions.
29 changes: 8 additions & 21 deletions Aegis/Commands.lean
Original file line number Diff line number Diff line change
Expand Up @@ -110,27 +110,14 @@ def sierraLoadString (s : String) : CommandElabM Unit := do

elab "aegis_load_string " s:str : command => sierraLoadString s.getString

elab "aegis_set_path " s:str : command => do
let fp : System.FilePath := ⟨s.getString⟩
unless ← fp.pathExists do throwError "Could not find cairo directory"
modifyEnv (cairoPath.addEntry · fp)

elab "aegis_load_file " s:str : command => do
let filePath : System.FilePath := ⟨s.getString⟩
let filePath ← toCallerRelativeFilePath filePath
match filePath.extension with
| .some "sierra" => sierraLoadString <| ← IO.FS.readFile filePath
| .some "cairo" =>
let filePath ← IO.FS.realPath filePath
let args : IO.Process.SpawnArgs :=
{ cmd := "cairo-compile"
args := #["--replace-ids", filePath.toString] }
let child ← IO.Process.output args
dbg_trace "Compilation stderr: {child.stderr}"
dbg_trace "Compilation stdout: {child.stdout}"
sierraLoadString child.stdout
| _ => throwError "Wrong file extension, must be .cairo or .sierra!"

elab "aegis_load_file " path:term : command => do
let str ← Elab.Command.liftTermElabM do
let path ← unsafe Elab.Term.evalTerm System.FilePath (.const ``System.FilePath []) path
let srcPath := System.FilePath.mk (← readThe Core.Context).fileName
let some srcDir := srcPath.parent
| throwError "cannot compute parent directory of '{srcPath}'"
IO.FS.readFile (srcDir / path)
sierraLoadString str

elab "aegis_info" name:str : command => do -- TODO change from `str` to `ident`
let env ← getEnv
Expand Down

0 comments on commit d391197

Please sign in to comment.