Heime (May 02 2024 at 22:35): Heime (May 02 2024 at 22:35):Have tried to build the target for lean, but one cannot easily build from source. There is no stable version yet. Seems to me that coq is much better. What do people think about this ? Especially from those who have worked with both coq and lean.
Mario Carneiro (May 02 2024 at 22:37):Please do not try to start fights like this.
Mario Carneiro (May 02 2024 at 22:39):As for the substance of the question, it is true, Coq is a much older and more mature software + ecosystem, and is considerably farther along in its stability arc than lean. It is not true that lean has not had a stable version though, it is currently on stable 4.7.0.
Heime (May 02 2024 at 22:40):Why is it always like this with all you people !!!!! This obsession of not saying that a child is ugly.
Mario Carneiro (May 02 2024 at 22:42):Most of the build complications stem directly from the decision to be self-hosting. This has many upsides and is not a particularly uncommon choice for programming languages, but Lean is self-hosting and Coq is not, which means that the build process is a bit more... well-founded... in Coq land. It is perfectly possible to build lean from source though, you were pointed directly to the instructions to do so on the lean zulip and as far as I am aware you were successfully able to do so.
Heime (May 02 2024 at 22:42):One of the Lean Community said there is no stable version yet. I have no idea. Anyway. With Coq I was able to see it show up in Synaptic.
Mario Carneiro (May 02 2024 at 22:45):Lean takes a similar approach to Rust in this regard (you also won't find rustc on Synaptic). Instead, the version manager (elan for lean, rustup for rust) is on the package registry, and you use that to install the right version. Coq also has a versioning situation but in my experience it is rather more manual with ocaml switches in opam. I will let others speak to that.
Heime (May 02 2024 at 22:45):Well, with all the mathlib complications I just gave up on it. It has been a few days of struggle to build it. Could always try it again in a couple of years.
Mario Carneiro (May 02 2024 at 22:46):That's your choice. If Coq fits your requirements better, don't let me stop you.
Heime (May 02 2024 at 22:49):With coq I have been able to run same examples using the CoqIDE within a couple of hours.
Heime (May 02 2024 at 22:50):Do you work with lean often, @Mario Carneiro ?
Mario Carneiro (May 02 2024 at 22:50):Yes
Heime (May 02 2024 at 22:51):Did you work with coq for some time as well ?
Mario Carneiro (May 02 2024 at 22:51):Yes
Mario Carneiro (May 02 2024 at 22:52):Following the instructions you can generally get lean + mathlib ready to use on a new machine in about 15 minutes. I think it's about the same for Coq, although I haven't tried walking anyone else through the new user flow for Coq
Mario Carneiro (May 02 2024 at 22:54):It is of course much more than that for many users because they either don't find the directions to follow, follow the wrong directions, or don't want to follow the directions. Usually the best case scenario is when the instructor is leading a group of people through the installation
Heime (May 02 2024 at 22:54):As I am having some success, I will get some prover experience with coq for now.
Heime (May 02 2024 at 22:56):Is there a mathematical reason that makes you work more with lean ?
Heime (May 02 2024 at 22:58):The next things I want to do is play with coq from emacs as I am one of its developers.
Mario Carneiro (May 02 2024 at 23:00):There are many usability reasons I prefer lean, but as far as mathematical reasons? They are quite similar, logically speaking. It will be quite some time before you run into any differences, but they do exist. If you are actually interested you can find a writeup of differences between Coq and Lean formal systems in section 2.8 of my masters' thesis about the lean formal system
Heime (May 02 2024 at 23:01):That's fantastic. Thank you so very much.
Heime (May 02 2024 at 23:13):Are you aware of any books or papers which focus on the development of provers in general ? Rather than on specific implementations ?
Heime (May 02 2024 at 23:49):For some instance I thought we had Jim Morrison here. Am an old sod from the 80's actually. Few people know this. We are usually every young programmer's nightmare.
Huỳnh Trần Khanh (May 03 2024 at 01:10):hey I saw you mentioned CoqIDE. please stop using it
Huỳnh Trần Khanh (May 03 2024 at 01:10):coq-lsp is better
Huỳnh Trần Khanh (May 03 2024 at 01:11):https://github.com/coq-community/manifesto/issues/145
Huỳnh Trần Khanh (May 03 2024 at 01:14):I think someone here hacked together a way to integrate coq-lsp with emacs, you probably can search this Zulip
Heime (May 03 2024 at 01:18):There is Proof General for emacs. But have not installed it yet.
Huỳnh Trần Khanh (May 03 2024 at 01:20):I know. it also uses that deprecated XML protocol like CoqIDE
Huỳnh Trần Khanh (May 03 2024 at 01:20):doesn't mean it's unusable but the experience might not be as good as coq-lsp and VsCoq2
Huỳnh Trần Khanh (May 03 2024 at 01:22):ugh... a lot of people here are also pretty old :) not me tho
Heime (May 03 2024 at 01:24):It does seem not to be as good. Is there any command line program to run files through through the coq prover ?
Mario Carneiro (May 03 2024 at 01:24):That's coqc
Heime (May 03 2024 at 01:25):A sort of automated output rather than an interactive IDE.
Mario Carneiro (May 03 2024 at 01:26):But one of the main draws of interactive theorem provers is the interactive aspect. If you try to compile everything from scratch the development workflow is much reduced
Huỳnh Trần Khanh (May 03 2024 at 01:28):not just much reduced it's more like you have no idea what's going on at all
Mario Carneiro (May 03 2024 at 01:28):This kind of workflow is much more realistic in "plain old" programming languages like C compared to Coq where compiling a file involves running many complex and expensive metaprograms (tactics). But it depends on the kind of code you are writing; many files still have quite reasonable compilation times
Heime (May 03 2024 at 01:28):The problem of the interactive aspect is that one has to run through each command to see the output produced, one by one. Rather than a complete listing of each status.
Mario Carneiro (May 03 2024 at 01:28):No?
Huỳnh Trần Khanh (May 03 2024 at 01:29):hey that's the XML mentality. the LSP based tools work differently. they analyze the whole file and cache the results at every point
Mario Carneiro (May 03 2024 at 01:29):Some of the IDEs (proof general and CoqIDE IIUC) work like this, where you can step through the proof one line at a time, but coq-lsp and vscoq work more like Lean/Isabelle where you see all errors in the file at once with red squiggles
Mario Carneiro (May 03 2024 at 01:32):But more importantly, you really want to be able to see the proof context when you are in the middle of the proof, and I don't think you get a very good view of this if your only interface is running coqc repeatedly while having the .v file open in Emacs
Heime (May 03 2024 at 01:40):That is quite an innovation.
Huỳnh Trần Khanh (May 03 2024 at 07:04):Seems to me that coq is much better. What do people think about this ?
Lean is a formidable opponent.
Huỳnh Trần Khanh (May 03 2024 at 07:06):The Coq community members are working really hard to compete with Lean.
Gaëtan Gilbert (May 03 2024 at 07:09):Huỳnh Trần Khanh said:
I know. it also uses that deprecated XML protocol like CoqIDE
not true (except for some branch that AFAIK is pretty dead), it uses coqtop
Pierre Roux (May 03 2024 at 08:16):Mario Carneiro said:
many files still have quite reasonable compilation times
My understanding is that this is much more true in Lean/mathlib, due to limitations of the IDEs. In the Coq ecosystem it's not uncommon to have multi-thousand-lines long files with compilation times that can then exceed the minute.
Mario Carneiro (May 03 2024 at 08:23):Lean files can definitely have minute plus compilation times too. My impression was actually that Coq was less heavy, although as you point out this is dependent on the style of the development and very long files or files using heavy tactics can make things take longer - it's really up to the patience of the authors multiplied by the overhead of their chosen interface.
The document model interface is better when whole file compilation is relatively fast or there is a lot of available computing resources, and the iron curtain interface is better when individual tactics are expensive and you don't want to run things more times than necessary. Conversely, developing things with the iron curtain interface decouples the whole file cost from the level of interactivity and responsiveness, so one would expect such files to be very long and very heavy, comparatively speaking. When I looked around I didn't find a lot of such files but I was probably just looking in the wrong place (e.g. stdlib)
Last updated: Oct 13 2024 at 01:02 UTC