read term from file

Stream: lean4

[Ciprian Teodorov]

Hi all,

is there a way to read a term from a file in Lean4?

The simplest example would be the following:

structure TestS :=  (name : String)
def ss :TestS := ⟨ "toto" ⟩

def main (args: List String) : IO Unit := do
  let fileName := args.head!
  let s : TestS := readTermFromFileName fileName
  IO.println s!"Hello, {s.name}"

Note that the function readTermFromFileName gets the name at runtime, and not at compile time.
I managed to write a tactic that works with a statically known filename like in the following:

def main (args: List String) : IO Unit := do
  let s : TestS := by { readTermFromFileName "test.lean" }
  IO.println s!"Hello, {s.name}"

But I have a hard time understanding how to generalize this approach with a statically unknown filename.

Best regards.
--
ciprian

[Mario Carneiro]

#mwe

[Mario Carneiro]

what does readTermFromFileName do?

[Mario Carneiro]

What is the storage format in the file you are reading?

[Mario Carneiro]

You can parse JSON into an arbitrary data structure fairly easily with deriving FromJson on TestS, but if you want to parse lean syntax you will have to load an environment from somewhere to use with the elaborator

[Ciprian Teodorov]

Mario Carneiro said:

what does readTermFromFileName do?

fileName is a path to a file which contains a lean term as string like ⟨ "toto" ⟩

[Ciprian Teodorov]

Mario Carneiro said:

You can parse JSON into an arbitrary data structure fairly easily with deriving FromJson on TestS, but if you want to parse lean syntax you will have to load an environment from somewhere to use with the elaborator

I do not want to pass through JSON.
Yes I guess we need an environment for the elaborator. Here is a more detailed example

import Lean
open Lean

structure TestS :=
  (name : String)
def nothing: TestS := ⟨ "nothing" ⟩
def s₁ :TestS := ⟨ "something" ⟩ -- the contents of the file are ` ⟨ "something" ⟩`

def readTermFromFileName(fileName: String) : IO $ TestS := do
    let code ← IO.FS.readFile ⟨ fileName ⟩
    initSearchPath (← Lean.findSysroot) ["build/lib"]
    let env ← importModules #[ ] {}
    let estx := Lean.Parser.runParserCategory env `term code
    match estx with
      | Except.ok stx =>
        let s1 : TestS := sorry -- How to get from stx to TestS ?
        return s1
      | Except.error e => return nothing
def main (args: List String) : IO Unit := do
  let fileName := args.head!
  let s : TestS ← readTermFromFileName fileName
  IO.println s!"Hello, {s.name}"

The question is how to get from the Syntax object returned by the parser to the TestS object.

an even more detailed example, that uses a tactic to read from a statically known filename is at: https://tinyurl.com/yawevj96

[Mario Carneiro]

Here's a working example.

Test.lean:

import Lean
open Lean

structure TestS where
  name : String

open Lean Elab Command

def runCommandElabM (env : Environment) (x : CommandElabM α) : IO α := do
  let cmdCtx := {
    fileName     := "<empty>"
    fileMap      := .ofString ""
    tacticCache? := none
  }
  match (← liftM <| EIO.toIO' <| (x cmdCtx).run { env, maxRecDepth := maxRecDepth.defValue }) with
  | .ok (a, _) => return a
  | .error e =>
    throw <| IO.Error.userError s!"unexpected internal error: {← e.toMessageData.toString}"

unsafe def readTermFromFileName (fileName : String) : IO TestS := do
  let code ← IO.FS.readFile ⟨fileName⟩
  initSearchPath (← Lean.findSysroot) ["build/lib"]
  -- this should be the name of the current module, or the one that contains the `TestS` definition
  let env ← importModules #[`Test] {}
  runCommandElabM env <| runTermElabM fun _ => do
    let .ok stx := Lean.Parser.runParserCategory env `term code | throwError "parse error"
    let ty := .const ``TestS []
    let e ← Term.elabTerm stx (some ty)
    Meta.evalExpr TestS ty e

unsafe def main (args : List String) : IO Unit := do
  let fileName := args.head!
  let s : TestS ← readTermFromFileName fileName
  IO.println s!"Hello, {s.name}"

lakefile.lean:

import Lake
open Lake DSL

package test

@[default_target]
lean_exe test where
  root := `Test
  supportInterpreter := true -- this is important

input.txt:

⟨ "something" ⟩

run as:

$ lake exe test input.txt
info: [0/2] Building Test
info: [1/2] Compiling Test
info: [2/2] Linking test
Hello, something

[Ciprian Teodorov]

Nice incantation.
Thanks a lot Mario, I'll play with it tonigh :wink:

[Adrien Champion]

This works quite well as long as it runs in the source directory, but how about running it as a standalone somewhere else?

[Adrien Champion]

Would you need to have some ~/.config/myProgram folder where you would put your sources/compilation artifacts (?) so that you have access to it when loading terms?

[Mario Carneiro]

you can use lake env to set up LEAN_PATH to find the necessary oleans for loading terms at runtime

[Mario Carneiro]

As long as you only depend on syntax from lean core you can probably also just depend on the oleans provided by the lean in the PATH

[Adrien Champion]

Here is a plug-and-play repo with Mario's code for current and future readers

[Adrien Champion]

Okay so the first time it runs, the program would typically create some ~/.config/myProgram folder, put olean/sources there. Then just make sure to set its LEAN_PATH so that term loading can find everything and it should work fine

[Adrien Champion]

Thanks!