How to Separate Header Loading With Running Commands?

Stream: lean4

[zmkm]

In the implementation of the lean server, files are reprocessed based on what the user has changed. I would like a way to reprocess the file whereby the headers stays the same (guaranteed), but the rest of the file's content (i.e. proof of the theorem) is changed. So I want to keep header in memory but adjust the commands, how to do this?

I have looked at https://github.com/leanprover/lean4/blob/master/src/Lean/Language/Lean.lean but I still can't make out how to do this.

[Michael Rothgang]

Question from the peanut gallery: is what you're asking related to the (future, in progress, experimental) module system Lean's supposed to get?

[Eric Wieser]

Usually these questions are related to building some kind of AI system

[Auguste Poiroux]

Lean REPL might be what you are looking for. Although, you will have to separate the imports from the rest of the code. The idea:

1. Process your file content by splitting it in 2: header, and rest of the file
2. Send the header to the REPL: {"cmd": "<header-code>"}. You should get back something like {"env":0}
3. Send the rest of the file content: {"cmd": "<file-content>", "env": 0}
   If your file content change, just repeat 3 with the new content and "env":0 again. The parameter "env" allows you to execute new code while keeping in memory what has been executed in the previous commands.

[Auguste Poiroux]

If you want to do it programmatically with Lean, you can probably borrow some code from this file: https://github.com/leanprover-community/repl/blob/master/REPL/Frontend.lean