Is there some "pure" function that reads a file before the program is type-checked and returns its contents as a string or something, for example if the file file.txt has the contents hello then I could write

example : readFile "file.txt" = "hello" := rfl

The reason I am asking is because I would like to implement a domain-specific language that compiles to a proof of something in Lean. For example if the file has a proof then I could write

example : 2 + 2 = 4 := interpretProof (readFile "file.txt")
/- or -/
theorem p : thingProvedBy (readFile "file.txt") := interpretProof (readFile "file.txt")
#check p -- p : 2 + 2 = 4

The alternatives that I can think of would be to (a) compile the DSL into Lean code and import it or (b) implement the DSL using the Lean macro system so that it can be written directly in a Lean program.

  • $\begingroup$ IO is never “pure”. Nonetheless, you can use meta programming to achieve at least some of your goal. In Lean 3 you can either write a tactic which reads from a file or make a custom user command. In Lean 4 I’m sure there are also similar options, likely involving macros or custom tactics. $\endgroup$
    – Jason Rute
    Jul 5, 2022 at 2:16
  • $\begingroup$ I or someone else might be able to tell you exactly how to achieve your goal but it will be different for lean 3 or lean 4. Can you edit your question to be clear on which one your are interested in? $\endgroup$
    – Jason Rute
    Jul 5, 2022 at 2:40
  • 1
    $\begingroup$ Tag (and mention of the macro system, which personally would be my favorite solution, naturally) suggest Lean 4. In that case, see github.com/leanprover/doc-gen4/blob/… (impl: github.com/leanprover/doc-gen4/blob/main/DocGen4/…) for such a term elaborator. Having said that, if you go this course, you might want to make interpretProof part of the metaprogram as well for performance. $\endgroup$ Jul 5, 2022 at 7:42
  • $\begingroup$ Why do you want DSL proofs to be in separate files? That sounds very annoying for anyone who will have to write these. $\endgroup$ Jul 6, 2022 at 8:45
  • $\begingroup$ Because they may use syntax that isn't supported by Lean's macro system. Having them in separate files would also enable one to implement syntax highlighting for the DSL. $\endgroup$ Jul 6, 2022 at 14:35


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.