linux command line

Stream: general

[Tim Daly]

I downloaded the 3.4.2 tar.gz image of lean and unpacked it into a directory, which contains only bin, include, and lib. In bin there is an executable called 'lean' which apparently does nothing. I've used lean in the browser and want a command line version on my linux box.
Can someone point me to instructions to actually run this executable? Google searches have turned up nothing.

[Simon Hudon]

What do you see if you run lean -v?

[Tim Daly]

Lean (version 3.4.2, commit cbd26686ddb, release)

[Simon Hudon]

So you have lean. You can call it on a file to check it and call lean --help to see the options

[Simon Hudon]

You might rather use it in emacs or VS code

[Tim Daly]

Thanks. I am looking for console interactions because I'm trying to feed it I/O from a lisp program.

[Simon Hudon]

There is also a C API if want to go that way

[Tim Daly]

I'm trying to use it "underneath" the Axiom compuer algebra system, essentially feeding it input and capturing the output. The "-server" command seems unhappy with "import system.io".

[Tim Daly]

It looks like the linux version has no "console" I/O.

[Tim Daly]

I'll look at the source code and see if I can hack something up. Sigh.

[Simon Hudon]

You can look at the way emacs or VS code are setup to interact with it. That should help

[Tim Daly]

I'll do that. Thanks. I expected that a linux version of the program would follow the standard "pipeline" model of interaction.

[Simon Hudon]

It doesn't seem flexible enough to make a language server

[Reid Barton]

In its basic mode lean is essentially a compiler, which can also run your program for you (lean --run)

[Tim Daly]

There is no such thing as a simple job...

I suppose I could create tmp files and do everything through the file system.

[Keeley Hoek]

Does fopen work on a unix socket?

[Bryan Gin-ge Chen]

There's a bit more information / links regarding the lean --server mode in this thread.

[Reid Barton]

Does fopen work on a unix socket?

If you want to play that game you can just do lean /dev/stdin

[Tim Daly]

re: fopen .... yes

[Reid Barton]

however I suspect Lean will want to read the whole input before producing any output

[Tim Daly]

the -run option wants "main" but I don't see a reference to main in the book "Theorem Proving in Lean", nor in the online tutorial. Can anyone point me at a working "-run" example file?

[Bryan Gin-ge Chen]

Leanpkg is one example: https://github.com/leanprover/lean/tree/master/leanpkg

[Tim Daly]

lean /dev/sdtin almost works

[Tim Daly]

This sorta-kinda-almost works:

lean /dev/stdin
import system.io
variable [io.interface]
open io

def main : io unit :=
put_str "hello world\n"

main
ctrl-d

except that it doesn't seem to like the put_str type and it says "too may arguments"

but, hey, progress!

[Tim Daly]

The above code is the first example from the tutorial with hello_world changed to main

[Tim Daly]

And this "worked":

lean /dev/stdio
import system.io
open io

def main : io unit := put_str "hello world\n"

#check main
ctrl-d

resulting in the output:
main : io unit

[Mario Carneiro]

lean doesn't work incrementally, it expects a complete file, so it seems a bit silly to be taking input on stdin

[Tim Daly]

Success!

lean /dev/stdio
import system.io
open io

def main : io unit := put_str "hello world\n"

#eval main
ctrl-d

resulting in the output
hello world

Many thanks.

[Mario Carneiro]

It also uses the location of the file to find relative imports

[Mario Carneiro]

so you are going to have trouble with nontrivial import statements

[Mario Carneiro]

also use triple backtick ```lean ... ``` to bracket lean text

[Tim Daly]

Mario, the problem is that I'm using I/O from Axiom, not from a file.

[Mario Carneiro]

then use Axiom to write to a file that exists somewhere in the intended import hierarchy

[Mario Carneiro]

what are you trying to get lean to do? What kind of input are you expecting to feed it?

[Tim Daly]

Axiom creates dependent types "on the fly" in the interpreter so there isn't (normally) an associated file

[Mario Carneiro]

lean --run foo.lean is essentially the same as lean foo.lean except that lean adds the line #eval main at the end of your file

[Mario Carneiro]

This is useful for using lean as a programming language for standalone executables

[Mario Carneiro]

If you are just proving theorems, you don't need it

[Tim Daly]

Yep. lean --run hello.lean works.

I'm looking to feed a lot of things into lean, and indeed, using lean for checking Axiom's spad code generated from a compiler back-end

[Tim Daly]

I'm proving Axiom's algorithms correct and trying to use Lean as the proof machine. So I need to "converse" with it.

[Tim Daly]

Lean's axioms and lemmas will come from Axiom's type hierarchy, along with tactics. They won't exist in files.

[Mario Carneiro]

Why don't you spit all the proof obligations into a file and then check it?

[Mario Carneiro]

what's the "conversation"?

[Tim Daly]

File I/O is possible but ugly. It's the late 90s. We can do better. (Just my opinion, actually)

Axiom interacts with other tools, like a browser, without file I/O

[Mario Carneiro]

You can communicate using memory only files using the server mode, but it's still not clear to me what conversation you want to have with lean. It's not particularly chatty when it comes to verifying a theorem is correct - the answer is either "yes" or a spew of errors

[Tim Daly]

I'm trying to learn lean programming. I'm pondering "compiling to lean" as one of the compiler backends. Of course, the user's program won't pass the compiler(s) (Axiom or Lean's) and I'll have to give feedback.

[Mario Carneiro]

If you want to "compile to lean" then you should clearly be writing to a file

[Tim Daly]

Axiom can compile "on the fly" from the command line. In fact it does so when resolving parametric types.

If you define f(x) == x*x then the call f(3) will compile an integer version and f(3.0) will compile a float version, all "on the fly"

[Tim Daly]

Everything could be done through files, I agree.

[Mario Carneiro]

I don't think lean will care about that. From lean's point of view that's just one function

[Tim Daly]

but f("noise") should fail

[Mario Carneiro]

That doesn't map very easily to lean's type theory, although it can be done

[Mario Carneiro]

lean uses typeclasses for that sort of thing

[Tim Daly]

I suspect Axiom's dependent type machinery is going to give lean a bit of trouble. But that's pretty much my own research problem.

[Mario Carneiro]

In any case, I would recommend using lean as a compiler, as Reid suggested. Don't try to start it up on every REPL line

[Tim Daly]

Does the emacs interface use files?

[Tim Daly]

In unix, a file is nothing more than a stream of bytes anyway

[Reid Barton]

The emacs mode uses --server, which you could also use yourself, but fundamentally it's not that different than invoking Lean on the entire file repeatedly

[Reid Barton]

It might be possible to implement a REPL in Lean without too much difficulty