Does Lean have a function that reads a file "at compile time"?

Question

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.