pure IO

Stream: lean4

[Jason Gross]

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]

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]

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]

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]

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]

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]

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]

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

[Jason Gross]

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]

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

[Jason Gross]

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]

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]

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

[Jason Gross]

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]

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]

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]

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]

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]

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

[Sebastian Ullrich]

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]

That is how the language server works:

Ah, neat, thanks!

[Jason Gross]

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]

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]

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

[Sebastian Ullrich]

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]

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]

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]

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]

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.