Zulip Chat Archive

Stream: lean4

Topic: pure IO


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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...)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.)

view this post on Zulip Sebastian Ullrich (Mar 20 2021 at 17:26):

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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Sebastian Ullrich (Mar 21 2021 at 14:34):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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) :) .

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Jason Gross (Mar 22 2021 at 14:13):

That is how the language server works:

Ah, neat, thanks!

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Jason Gross (Mar 22 2021 at 14:17):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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