web editor

Stream: general

[Patrick Massot]

@Bryan Gin-ge Chen in your version of the web editor, is it possible to get only tactic state and not all messages?

[Patrick Massot]

I tried https://bryangingechen.github.io/lean/lean-web-editor/#url=https%3A%2F%2Fraw.githubusercontent.com%2FPatrickMassot%2Flean-tutorials%2Fmaster%2Fsrc%2Ffirst_proofs.lean and it works great but displaying all messages at once is really confusing

[Bryan Gin-ge Chen]

Not at the moment but I can try to add that functionality. Any UI preferences?

[Patrick Massot]

There could be a switch somewhere, but it should also be configurable in the url, so we can link to tutorials having the expected behavior (or else make that behavior the default one)

[Bryan Gin-ge Chen]

Sounds good, I'll see what I can do.

[Patrick Massot]

Thanks!

[Bryan Gin-ge Chen]

@Patrick Massot I ended up copying the behavior of the vscode extension (and stole the icons too). Give it a try now (you may need to clear your cache).

[Patrick Massot]

It works!

[Patrick Massot]

Thanks!

[Patrick Massot]

It looks like VScode, except it still displays "no goals", which feels old-fashioned...

[Patrick Massot]

:wink:

[Bryan Gin-ge Chen]

Also easily fixable... maybe in the next update.

[Kevin Buzzard]

I want to be able to post a theorem from my algebraic geometry course as something that people can play with using the Lean web editor. My problem is that I want to post a super-non-intimidating-for-mathematicians file, which needs some other imports in the repo which are of a far more CS nature. Basically I only want the students to see the interface. I don't have time with mathlib PR's for this stuff, my code works fine for me and I'm sure it's not mathlib-ready. One cheap fix, however, would simply be to cut and paste all the imported code used above the code I want them to see, in one big file, and then put the "imported" code into some invisible box which is not displayed on the web editor. Line numbers will be weird but I don't care. Can this be done?

[Johan Commelin]

@Bryan Gin-ge Chen I guess that at least in ObservableHQ this is easy, right?

[Reid Barton]

You'll have to do something a little bit cleverer than that if you want the user to be able to use import, since as you describe it the imports won't all be at the top of the actual file that Lean sees, then

[Johan Commelin]

No, I think Kevin suugests to avoid import, by literally copy-pasting the code. (Manual import, so to speak.)

[Johan Commelin]

He then wants to hide the copy-pasted code from the user, using some javascript magic.

[Bryan Gin-ge Chen]

Doing this with the community web editor would definitely require modifying the editor code. My impression was that @Mohammad Pedramfar's code for the natural number game supported something like this though.

I'll see if I can cook up an Observable notebook later tonight.

[Reid Barton]

Right but it means that import in the user's code will break. But perhaps this isn't an issue for you.

[Johan Commelin]

Yup. This quickly becomes messy.

[Kevin Buzzard]

There will be no import in the user's code. It will just be a one-off file to experiment with so that people can compare the Lean proof to the maths proof without having to install Lean. Bryan -- yes you're right, I could definitely do it with the Lean game maker. Maybe this is easiest!

[Tim Daly]

Having failed to install lean on 3 different systems, I turned to the Lean Web Editor, as mentioned in TPIL. Is there a page that says how to use it? I want to create a variable of type Integer, which seems to need \mathbb{Z}, but I don't know how to type it. Sigh.

[Chris Hughes]

You can just write int

[Tim Daly]

Where can I find more information about how to use this editor?

[Tim Daly]

Is there a Docker version of Lean?

[Yury G. Kudryashov]

Which OS?

[Yury G. Kudryashov]

I mean, on which OS did you try to install Lean?

[Tim Daly]

Ubuntu, MAC, Windows.

[Tim Daly]

Ubuntu, for example, complains during apt-get that the repos are insecure.

[Tim Daly]

The first google hit goes to a page that says to install git, libgmp-dev, and cmake... but nothing else.

[Tim Daly]

I "installed" lean on ubuntu and the ./lean binary "runs" but does nothing.

[Joe]

mac : https://github.com/leanprover-community/mathlib/blob/master/docs/install/macos.md
ubuntu : https://github.com/leanprover-community/mathlib/blob/master/docs/install/debian.md

[Joe]

I have no problem following these

[Tim Daly]

Once more, "with feeling", as my music teacher said.

[Bryan Gin-ge Chen]

Note that just running "lean" from the command line doesn't return any output. You can run lean -h instead to see the basic command-line help string. However, you most likely don't want to use lean solely from the command line. Instead, lean should usually be used interactively in conjunction with either VS Code or emacs. It looks like mathlib's "Creating a Lean project" doc assumes you want to use VS Code. If you prefer emacs, I guess you'd want to look here as well.

Also, the community version of the web editor has some instructions on how to input special characters if you click on the purple (?): https://leanprover-community.github.io/lean-web-editor

[Tim Daly]

Thanks. That worked. I've never seen anything require so many packages to install. I thought lean was a C++ program. No wonder my efforts to hand-install lean failed. My attempts to use emacs failed so I installed vscode.

[Tim Daly]

Is there some magic incantation to tell vscode to execute something like #check

[Bryan Gin-ge Chen]

Not sure what you mean. You type #check in front of the expression you want to type-check, in both the web editor and VS Code.

[Bryan Gin-ge Chen]

Something like this:

Screenshot-2020-01-25-21.20.26.png

[Tim Daly]

vscode was installed without the lean extension. I finally found it.

[Patrick Massot]

Thanks. That worked. I've never seen anything require so many packages to install. I thought lean was a C++ program. No wonder my efforts to hand-install lean failed. My attempts to use emacs failed so I installed vscode.

Indeed lean is a C++ program. The installation procedure is to go to the official website, search for a link called Download, then a link called binaries and click on the link relevant to your platform on https://github.com/leanprover/lean/releases/tag/v3.4.2. Then you need to know how to unpack a zip or tar.gz archive on your platform. Was that the blocking step?

[Patrick Massot]

Or maybe you mean that you didn't only want the Lean C++ program but also a lot of user-friendly supporting tool? Then you'll indeed need an editor, probably also an editor plugin talking to Lean. Maybe you also want to use Lean libraries created by other people. Then you'll need to download that as well, but this requires reading a bit more documentation, and maybe use python tools to make it easier. Then indeed you depend on quite a few packages, but only the Lean binaries are Lean itself.

[Patrick Massot]

All that being said, I'd be curious to learn more about "Ubuntu, for example, complains during apt-get that the repos are insecure.". What repos are you talking about?

[Tim Daly]

Ok, for background, I've been programming for 50 years and an open source lead developer since 1997. So, 'tar' isn't the issue.I've been using emacs since the late 70s so I have a 'user-friendly supporting tool'. For Axiom installs you only need to type 'apt-get install axiom' and then 'axiom'. Or, if you prefer, there is a Docker version of Axiom. All of the documentation is in PDF. I hardly know how to make it easier.

The usual game is to 'git clone the repo and type 'make' to get a useful system. The tar-make path leaves me with 3 binaries. The ./lean binary appears to do nothing. So I followed with a Google search, found the PPA extensions for apt, did the repo-setup / apt update, and the apt-get. But the PPAs appear to be unsigned so apt is unhappy. Similar losses on Mac and Windows (and Windows WSL). The Google search did not show me the 'wget' link. Being a trusting soul I executed that command sequence and (almost) got a useable system (modulo the emacs/vscode issue). I was just astonished at the number of packages, including whole languages like python, got installed.

Somehow Lean can talk to the vscode editor, can accept input, and show output. But apparently this won't work from the command line (or I'm just being too slow to understand). On Unix systems one tends to expect that programs accept stdin and write to stdout so that all of the other tooling 'just works'. Is there a way to point it at a file and just get the output?

Obviously, my mindset is the problem. To use Lean effectively I have to adopt a whole new tool chain. That is going to make it very painful to package and ship it as part of Axiom. I need things like test automation during build so proofs are checked at build time. I need the proof-checker available as a separate tool. I need to integrate the lean system with the Axiom command line so you can #check, for example.I realize, coming from the "other side" of computational mathematics, that I'm not the usual lean customer. Nevertheless, I feel it is important to merge Lean and Axiom seamlessly.

Rather than complaining, is there a way I can help?

[Tim Daly]

The first "tooling" of interest would be a way to take an input file and "compile it" to a fully elaborated proof that only needs the proof checker (no libraries, no tactics).The proof checker should accept that "compiled form" and accept or reject it.

[Tim Daly]

My understanding is that the proof checker only needs the trusted kernel as support.

[Jason Rute]

I do agree that using and installing Lean is very different from other apps. Part of this I think is that while lean is a compiler (and can compiler programs from the command line), its interactivity is what is more important. If you just want to check/compile a lean file from the command line, you can use lean my_lean_file.lean. However, Lean has no REPL. It does however have a server lean --server which can be used to communicate with it interactively by a machine. (It is unusable by a human directly.) I think this is how emacs and vs code communicate with Lean. The server is really designed for interactive and incremental checking of a lean file while it is being worked on and hence is frustrating to use for direct communication. However, some have been able to make Lean communicate with external processes that aren't editors by using the Lean server. For example, @Rob Lewis and @Minchao Wu have built a bi-directional connection between Lean and Mathematica.

I'm also building a small python prototype which I'm using to communicate with Lean directly for the purpose of machine learning. I'll put that on GitHub in a few days.

[Jason Rute]

To be clear, I think none of us think that installing Lean is as easy as it could be. And using Lean from an external application is a huge pain. I think the official word from Microsoft research is to wait for Lean 4. (And they won't let you make any changes to Lean directly except in your own fork.) However, I think as a community we can find work arounds and better documentation for Lean 3.

[Jason Rute]

The way I am using the Lean server (and I imagine how Rob and Minchao are also doing it) is to send a JSON sync request to the server and then wait not only for the response to that request, but also an "all_messages" response which contains any compiler errors. The round trip takes about 0.1 seconds which is pretty slow IMO. See more discussion on this topic. (Actually, you might want to check out that whole stream.)

[Tim Daly]

I built programs for Microsoft in the past. I used a commercial program that built ".msi" files (if memory serves) that could automatically install all of the programs in the right place. My customer set (Intel and Police) just wanted "point and click" installs. I'm surprised that a Microsoft-related Lean program doesn't have this tooling. In addition, the documentation had a LOT of pictures (about 2 per page) along with a lot of "click on the blue box now".

[Tim Daly]

re: the MMA-Lean link... why would you need to translate "x^2-2*x+1" into fully elaborated code? You have systems on either end that can parse expressions. I'm rewriting the Axiom system to accept / produce Lean proofs at the user-level source code.

[Tim Daly]

Axiom should store fully elaborated code that a proof checker can check. But that is never user visible. It is only used when the Axiom "Oracle" wants to supply an answer to Lean (e.g. a GCD result) so Lean can trust the answer.

[Jason Rute]

From my little experience, the usual Lean output is not easy to parse by a machine. However one can write a custom parser for expressions, which is what they do. They could have made it more generic (like s-expressions or JSON), but I guess they wanted to directly put the AST into Mathematica code.

[Jason Rute]

In your system @Tim Daly what would you be sending to Lean and what would you be getting back? Are you sending a proof of a specific result, like theorem xx123 : nat.gcd 6 9 == 3 := <some proof>? Are you just getting back just something indicating whether that proof is correct or not? Or is it more complicated?

[Tim Daly]

Thanks for the Lewis/Wu paper link. I know what I'm doing for the rest of the day.

[Tim Daly]

re: Lean/Axiom communication. These are "peer" systems so each needs/provides services. Axiom has 10k algorithms that need to be proven correct so it needs Lean (and an associated "computer algebra" mathlib-like library on the Lean side). Lean needs to be able to use heavy algorithms (like Groebner basis) with the associated proof so it can get "Oracle" answers. I am not at the stage of defining the communication link.

But (I think) Lean is the combination of a trusted core, and as of Lean 4, the rest of it will be Lean code. If that is the case it should be possible to re-implement the trusted core in Lisp and embed all of Lean inside Axiom. That way there is no "communication link" as each system has shared data representations.

[Tim Daly]

Instead of being "a proof system" and "a computer algebra system", it becomes a "computational mathematics" system.

[Jason Rute]

By the way, in Lean 4, I think instead of this custom JSON server, they will switch to the Language Server Protocol. I don't know that it will change much, but Lean 4 might also make it quicker and easier to communicate with Lean.

[Jason Rute]

As for the proving and running algorithms, will they be running in Axiom or Lean? For example, the user wants a calculation of gcd 6 9. Would that calculation be done in Axiom with an algorithm verified by Lean offline to be correct? Would that calculation be done entirely in Lean? Or would Axiom compute some sort of proof witness that would be checked in Lean? (I'm not sure what that would be for gcd, but for an integral it could be a proof that the integrand is the derivative of the Axiom computed solution.)

[Tim Daly]

One of the key problems with the idea of a peer-to-peer communication interface is context. Axiom allows full runtime, first class dependent type construction. So the types are "part of the session". Since dependent types are undecidable Axiom uses built-in heuristics to resolve types at runtime. That mean, of course, that if you try to communicate the expression "x^2-2*x+1", you also have to communicate the type of "x" and the type of the coefficient ring (is it modular?) as well as the type of the whole expression.

Merging Lean and Axiom in a common system means that the runtime dependent types are shared and Lean can know that this is a polynomial with coefficients mod p. Similarly, the question above about doing integration means that Lean has access to Axiom's implementation of the Risch algorithm.

[Patrick Massot]

Tim, my message was specifically answering "I've never seen anything require so many packages to install. I thought lean was a C++ program." Of course I would like the supporting tools to be easier to install. But Lean itself is trivial to install.

[Patrick Massot]

As for the "I'm surprised that a Microsoft-related Lean program doesn't have this tooling." rant, I think you are confused by the relation between Microsoft whose business is to sell software to users and Microsoft Research where Leo is working on a research project that is not looking for users yet.

[Patrick Massot]

The Lean community is certainly trying to attract users, but Microsoft research is not.

[Patrick Massot]

Now let's try to improve things. You wrote you found a Lean PPA. I tried to google it and found https://launchpad.net/~leanprover/+archive/ubuntu/lean. Is that what you found? It doesn't seem too dangerous since it says the last build was in 2016, but of course it could still fool a couple of people. Does anyone know how we could take it down? Or even better, get write access? Does anyone know how to reach Soonho Kong nowadays?

[Sebastian Ullrich]

Thanks for pointing this out. @Leonardo de Moura made the PPA inaccessible, it should soon be deleted completely!

[Patrick Massot]

The first "tooling" of interest would be a way to take an input file and "compile it" to a fully elaborated proof that only needs the proof checker (no libraries, no tactics).The proof checker should accept that "compiled form" and accept or reject it.

That is already available: lean myfile.lean --export=myexportedfile.

[Tim Daly]

I don't expect that Leo is the person doing the tooling. If I still had access to the MSI tool I would try to remember how to create a windows install file. I'm also thinking of making a Docker image, as I did with Axiom. First I have to get a few clues about the details of fighting with the machine. But I think that a Docker image would be most useful as it installs and runs on every platform.

[Tim Daly]

Wow. A 10 megabyte output file for a 3 line program. Us there a file description somewhere?

[Jason Rute]

Running the Lean server (or the Lean command line) from Docker should be easy. Lean in Emacs might also be straight forward if you use the command line Emacs (and have it running inside Docker). Would we be able to easily set up Lean for VS Code with Docker?

[Jason Rute]

The first "tooling" of interest would be a way to take an input file and "compile it" to a fully elaborated proof that only needs the proof checker (no libraries, no tactics).The proof checker should accept that "compiled form" and accept or reject it.

You might be interested in @Mario Carneiro's MM0. The idea is that it is a sort of "assembly language" for proof assistants (or a trusted core) for which one could "compile" Lean code (or that of any other proof assistant). It should be relatively easy and quick to check MM0 code. (The hard part is actually writing the Lean to MM0 "compiler", and checking that the MM0 proof is a proof of what you think it is.)

[Mario Carneiro]

My plan is too hook up @Chris B's nanoda to the lean.mm1 axiomatization with a bit of proof logging for things like definitional equality proofs. Almost all the missing pieces are in place for this, although I haven't started working on this pipeline specifically yet

[Chris B]

@Mario Carneiro It took me a while to get the Lean3 -> lean4 changes working since they went deeper than I thought, but I got those done since we last spoke and literally just finished the first version of the revised tracing branch a few hours ago.

[Chris B]

Well the first version I don't hate. I'll polish it up some more by the end of this weekend.

[Mario Carneiro]

Are the lean 3 -> 4 changes backward incompatible?

[Chris B]

@Tim Daly If you're talking about the export file's size, it's because the export file includes the prelude + your stuff. The prelude's export file only takes a few seconds to parse and check. You can read about what the stuff in the export file means (and maybe get some insight into how the kernel sees Lean terms) here https://github.com/leanprover/lean/blob/master/doc/export_format.md
Fun fact, Mathlib's export file is ~230 mb and > 8 million lines.

[Mario Carneiro]

Oh, that helps a lot to guess how it compares with set.mm

[Mario Carneiro]

which is 30 MB compressed

[Mario Carneiro]

I'm glad to hear there is only one order of magnitude difference, I was worried the tactic proofs might be a lot worse than that

[Mario Carneiro]

when you throw in defeq proofs it will probably double in size

[Chris B]

@Mario Carneiro They're incompatible in that the code that I wrote is hella different, but the new version of nanoda can check lean3 export files.

[Mario Carneiro]

what's new in the kernel?

[Mario Carneiro]

the lean.mm1 axiomatization doesn't cover mutual recursion (because the thesis version doesn't either)

[Mario Carneiro]

wait, is there such a thing as lean 4 export files?

[Mario Carneiro]

my understanding is that lean 4 has no export format right now and may ship without one

[Chris B]

They removed the whole concept of reduction rules in favor of what Sebastian referred to as hard-coded recursors for both inductive and quotient, there's some new gadgetry for mutual definitions, and some of the typechecker stuff is different, esp the procedure for unfolding/delta reduction. I think the C++ version of lean3's checker was closer.

[Chris B]

Well the kernel has these new declaration types called Opaque, Theorem, and Mutual that are in the kernel but don't have any lean3 representation. So I've made code for them, but they don't appear in lean3 export files.

[Chris B]

Opaque and Theorem are similar to Definition.

[Chris B]

I forgot to ask Sebastian about them, but I was pretty sure they were meant to be lean 4 export items, like #OPAQUE ..., #THEOREM ... since they're in like the same 'class' of kernel item.

[Chris B]

Actually I think I did ask, but the kernel wasn't his wheelhouse so he wasn't sure. Or something.

[Mario Carneiro]

I guess these are like definition except the kernel won't unfold them? Or something?

[Mario Carneiro]

I assume that while heuristics etc for delta reduction may have changed the basic principle is still the same, so my thesis doesn't need to change there

[Chris B]

Oh abbreviation is the other one. Opaque and Abbreviation were like enum variants of ReducibilityHint in lean3, which dictates how definitions are unfolded yeah.

[Mario Carneiro]

Even Opaque definitions don't really change anything in the axiomatization since you can just say that they could be unfolded but aren't

[Mario Carneiro]

hardcoded inductives and quotients aren't really a problem, I mean they were basically hardcoded anyway with an "extensible" system with exactly two extensions and no external access

[Chris B]

There's also a new thing for handling all of the unique names, local_ctx, but I can only sort of pseudo-code read c++ and the implementation is over my head.

[Mario Carneiro]

Mutual sounds like something new though... an equation compiled definition understood natively by the kernel? Like Agda?

[Chris B]

The kernel only defines it as a type of declaration, it doesn't actually get used by the stuff you get in an export file, but the constructor gets called in the files that implement the equation compiler yeah.

[Mario Carneiro]

So the content associated with a Mutual declaration is the same as that of a regular declaration? (e.g. the lean 3 analogue being @[mutual] def foo := bar)

[Mario Carneiro]

and delta reduction works as normal?

[Mario Carneiro]

Did you implement any of this for nanoda, or are you just recognizing the (hypothetical) syntax?

[Chris B]

Most of it is implemented. The part of lean4's inductive that deal with nested inductive I haven't done yet since I wanted to get a C++ person's opinion on how local_ctx works, and the new declaration types exist but don't do anything because they're never called. w.r.t the mutual thing, from the kernel's perspective it's like a Vec<Definition> where Definition is the def my_thing : A := ... variety, and they're marked meta. The process for checking whether they're admissible is like iterating over them with the same procedure as for definitions.

[Mario Carneiro]

Oh, Mutual definitions are always meta? well in that case I will ignore them :P

[Chris B]

If they're being checked in the kernel at least.

[Tim Daly]

I've built a Docker version of Lean. Unfortunately it seems that hub.docker.com (hosted on amazon's cloud) seems to be down at the moment. Once I figure out some other path (or hub.docker recovers) I'll make it available.

[Jason Rute]

When you say a “Docker version of Lean”, can you use the docker version for vs code or emacs? If so, are they also running in the Docker container?

[Tim Daly]

vscode is installed in the docker. I am playing around with an emacs version. Hopefully I can get both in one image.

[Jason Rute]

I didn’t realize you could run a GUI from a Docker container. This will be interesting.

[Tim Daly]

Emacs runs fine. Apparently Docker has moved/merged with Kubernetes so I'm behind the curve on yet another technology. It takes forever to understand how to build one of these things so it might take a while. Kubernetes is more network capable . Axiom uses X11 for its graphics and browser front-ends and has used a remote X11 server successfully. I suspect there is a way to get vscode to "network" so I'm going to dig into that. I may be able to get lean --server to pipe to a network using ns. There are many "variables in play" here and I still have a lot to learn.
There won't be much more to say until I get happy with the results.

That said, I think that a Docker/(Kubernetes?) solution provides a trivial-to-install, stable platform for releases that run everywhere. I think that a Kubernetes version of Lean "in the cloud" is also possible, perhaps connected to @William Stein 's Sage system or the Jupiter notebooks.

I think that a "point and click" version of Lean would be easier for mathematicians and students to use.

[Johan Commelin]

That's one thing I have wanted to look into, but never actually got to it: Since VScode runs on electron, it should be easy to run the editor front-end on a simple laptop, and run the back-end (including Lean) on some heavy-duty server. Does anyone have a clue how hard it is to pull this off?

[Johan Commelin]

@Bryan Gin-ge Chen I think you also linked us to some "VScode in the browser" thing. Did that ever take off? I already lost that link, so I don't even know how to find the project atm.

[Bryan Gin-ge Chen]

The closest thing I can think of is the monaco editor which is what the lean-web-editor uses.

[Johan Commelin]

@Tim Daly re docker. I just unearthed this post by William Stein https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Installation.20and.20usage.20instructions/near/147247975

[Johan Commelin]

@Bryan Gin-ge Chen I think I found it: https://stackblitz.com/

[Bryan Gin-ge Chen]

OK, I don't think I've seen stackblitz before but it looks cool!

[Johan Commelin]

Ooh, maybe it was Patrick who showed it to me

[Tim Daly]

@William Stein is way ahead of me. Cocalc is certainly a better path than I'm taking, especially since it helps William and has real company backing. Anyone who has used Cocalc for Lean, please post instructions.

[Kevin Buzzard]

It works out of the box!

[Kevin Buzzard]

The only thing you need to know is that it reads leanpkg.path from the root directory and I believe this can't be changed

[Tim Daly]

Gotta love @William Stein 's work. He's a good guy and needs the support. Besides, now I can go back to being lost in Lean.