## Stream: lean4

### Topic: pure IO

#### Jason Gross (Mar 19 2021 at 20:51):

Is there a way to take something in the IO monad and run it on a "fake" world by filling out the relevant stubs for filesystem and environment interaction?

#### Sebastian Ullrich (Mar 19 2021 at 20:54):

There is not. We had a big monad class for IO operations in Lean 3, but no-one ever used it, and I think it was incomplete and/or hard to use anyway. It's much better to define a class of all operations you're interested in yourself and then give a pure and an IO instantiation.

#### Jason Gross (Mar 19 2021 at 21:00):

Er, my use-case for this is that I want to reuse the Lean compiler/frontend but run Lean in a sandbox where it's allowed to read from the environment and the filesystem and the current state of Lean, but where any write operations (to any of these) are replaced by no-ops. Is the current implementation of lean sufficiently parametric that I can do this?

#### Sebastian Ullrich (Mar 19 2021 at 22:29):

That sounds like a curious use case. Is it supposed to be sound? Lean programs can do arbitrary FFI, as well as break memory safety. I always imagined that if someone wanted to sandbox building Lean dependencies or something like that, they would do it from the outside with a proper sandbox.

#### Jason Gross (Mar 20 2021 at 01:39):

It doesn't need to be sound, just best-effort. My goal is to port my bug test-case minimizer from being a python script that works with Coq to bring a Lean program that works on Lean files. It won't be very effective if running a Lean script twice is different from running it once, so I'd like to isolate the effects as best I can. But it's not too important. (And I have many other problems to solve first, such as how to execute the lean program successfully in the first place...)

#### Joe Hendrix (Mar 20 2021 at 01:57):

Do you need to deal with a Lean program that modifies files? Could you just reset the files on a case-by-case basis? The other options I would consider if running the program in a container or attaching to the Lean process at startup with ptrace and intercepting all the calls to write and other system calls.

#### Jason Gross (Mar 20 2021 at 13:24):

Ideally the minimizer would work on any file that you give it. But, no, it doesn't need to work on programs that modify files

#### Sebastian Ullrich (Mar 20 2021 at 13:34):

Yeah, I would suggest to postpone that particular feature :) . But now I'm curious, does Coq provide something like that?

#### Jason Gross (Mar 20 2021 at 17:25):

Very few operations in Coq write to disk, none of them set the environment, and you can only read from disk to load a file. So it's pretty hard to make a non-idempotent operations involving the file system. As far as the state of the prover is concerned, I just spawn a new process for every run. (Btw, this is going to be an issue: I will need a way to contain the effects of things like set_option pp.all true, etc, so that they're reset before re-reading the file.)

#### Sebastian Ullrich (Mar 20 2021 at 17:26):

What do you mean by "reset"? They are not global mutable state.

#### Jason Gross (Mar 21 2021 at 14:25):

Ah, okay, that's good to know. But it seems like some state things are stored globally, e.g., the result of Lean.initSearchPath. Is there a way to change the search-path (or anything else like that) from within a Lean program?

#### Sebastian Ullrich (Mar 21 2021 at 14:34):

Is there a way to change the search-path (or anything else like that) from within a Lean program?

Yes, you can call initSearchPath at any point (again)

#### Sebastian Ullrich (Mar 21 2021 at 14:34):

That IORef might be a remnant of the cmdline driver that is still implemented in C++

#### Jason Gross (Mar 22 2021 at 13:41):

So if I run runFrontend on a program that does some imports and then does #eval Elab.initSearchPath (Option.some foo) and then does some more imports (presumably with the new search path?), then won't I be starting out in a different state the second time I call runFrontend, because the internal initSearchPath will have modified the search path for import?

#### Jason Gross (Mar 22 2021 at 13:42):

Or will there be two different levels of search paths, then, and there's no way to modify the outer one from the inner context?

#### Sebastian Ullrich (Mar 22 2021 at 13:47):

I see, yes, in that case the second run would see the updated search path of the first run. Is that a practical concern? It sounds unlikely unless you run the test case minimizer on itself (or similar programs) :) .

#### Jason Gross (Mar 22 2021 at 14:02):

It's probably not very likely, but I wouldn't be surprised if it happens at some point. (And if I hit a bug when writing the test-case minimizer, it would be nice to be able to run it on itself.)

#### Jason Gross (Mar 22 2021 at 14:06):

Another useful thing here would be to be able to run the minimizer in a mode optimized for long-running files, where instead of starting the execution from scratch at each run, the minimizer kept a cache of the execution state after each prefix of the document, and then resumed lean from the longest prefix that it had cached. (I assume that Lean might optimize things for linear usage, so perhaps it only makes sense to do this when the program takes "long enough" to run, or to have it be a command-line switch, but it would still be a nice thing to allow.) But this only works if I can handle FrontendM in a more pure way

#### Sebastian Ullrich (Mar 22 2021 at 14:10):

That is how the language server works: https://github.com/leanprover/lean4/blob/master/src/Lean/Server/Snapshots.lean

#### Sebastian Ullrich (Mar 22 2021 at 14:12):

Btw, the minimizer will not actually contain any #eval modifying global state, will it? I really don't think such programs are a practical concern since they will confuse the language server as well and should be avoided at all cost.

#### Jason Gross (Mar 22 2021 at 14:13):

That is how the language server works:

Ah, neat, thanks!

#### Jason Gross (Mar 22 2021 at 14:16):

Btw, the minimizer will not actually contain any #eval modifying global state, will it? I really don't think such programs are a practical concern since they will confuse the language server as well and should be avoided at all cost.

Usually, no. However, in the very rare case that there is a bug in how Lean executes programs in #eval and I hit this bug only on certain inputs to the minimizer, I may run the minimizer using #eval to exhibit the bug and then run the minimizer on this file that itself calls the minimizer via #eval.

#### Jason Gross (Mar 22 2021 at 14:17):

And, er, I was hopping to be able to write a test-suite for the minimizer in Lean, and I think the most effective way to do this would be with a bunch of #eval commands that invoke the minimizer...

#### Jason Gross (Mar 22 2021 at 14:17):

I suppose I can write add a switch that disables the call to initSearchPath, though

#### Sebastian Ullrich (Mar 22 2021 at 14:21):

Alright, I concede that running the minimizer on the test suite of a minimizer could run into this issue :laughing: . But even then, the result will probably be deterministic after all since you will most likely always call initSearchPath before the corresponding importModules call.

#### Sebastian Ullrich (Mar 22 2021 at 14:24):

Note that processing a Lean file multiple times in the same process is a bit fiddly anyway since imports have to be unloaded manually and unsafely: https://github.com/leanprover/lean4/blob/master/src/Lean/Environment.lean#L594-L597. This is hard to do correctly e.g. in the presence of async tasks, but for your specific purpose I don't think that should be an issue.

#### Jason Gross (Mar 22 2021 at 14:42):

Hm, will Lean handle this automatically for me, if I use the interface in Lean.Server.Snapshots? Or do I have to do something special to fiddle with imports? Also, how do I get my first snapshot? There doesn't seem to be a version of compileCmdsAfter which doesn't ask for a starting Snapshot...

#### Sebastian Ullrich (Mar 22 2021 at 14:45):

The initial snapshot is created here: https://github.com/leanprover/lean4/blob/3749213e08285d3a139da6cf04b30b5e38ed6179/src/Lean/Server/FileWorker.lean#L204
That function also shows how to use leanpkg to get at the LEAN_PATH.

#### Sebastian Ullrich (Mar 22 2021 at 14:48):

We actually have a separate server process per file, which we restart when the imports have changed. Much easier than manually stopping all spawned tasks.

Last updated: May 18 2021 at 23:14 UTC