jsCoq landing page · jsCoq · Zulip Chat Archive

Stream: jsCoq

Topic: jsCoq landing page

Emilio Jesús Gallego Arias (Feb 21 2022 at 14:57):

I am still reluctant to promote (accurately quantifiable by both qualitative and quantitative methods XD) inferior proving styles in the front page XD but indeed we should move from the current landing structure.

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:00):

now that you mention it Shachar we have been discussing about why math-comp is not accesbile and lean (which is very very similar is), now that the 10th anniversary of the feit thomsom proof is gonna happen

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:00):

but that's a topic for a different thread, the landing page, I agree, should be very different

Théo Zimmermann (Feb 21 2022 at 15:00):

@Emilio Jesús Gallego Arias "inferior proving style" is ill-defined. Inferior for what purpose is the question.

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:00):

@Théo Zimmermann as I mentioned, in the talk I didn't have time to give at the hackathon

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:01):

I have proposed both a qualitative and quantitative criteria, but I will still do this seminar soon

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:01):

it is not ill-defined in my case, you may agree or not, that's a different story

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:02):

I guess people don't grasp how gigantic the proofs of 4 color and FT are

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:02):

there are 5 lines lemmas in FT that contain more maths that full ITP papers

Théo Zimmermann (Feb 21 2022 at 15:02):

My point is that SSReflect/MathComp style can be considered superior for X, while being just inferior for Y.

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:02):

in terms of proof difficulty,

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:02):

sure I will discuss that, feel free to move this discussion to the proper topic and we can schedule my talk actually

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:03):

actually I could use a lot of your feedback I'm sure

Pierre-Marie Pédrot (Feb 21 2022 at 15:03):

Emilio Jesús Gallego Arias: there are 5 lines lemmas in FT that contain more maths that full ITP papers

That's precisely the problem, we don't want to teach that to beginners

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:03):

Most feedback I've had has been from interns that I taught

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:03):

I agree math-comp is not accesible

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:04):

but still, I can't teach my students a style that I know is not the one I prefer

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:04):

but let's move this to the right place please

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:04):

I agree with @Shachar Itzhaky about the landing page, I'm sure we can find a nice proposal that makes everyone happy

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:05):

"That's precisely the problem, we don't want to teach that to beginners" Lean is doing that and see how Lean vs Coq for the mathematicians is working

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:05):

The reality is that Coq for maths sucks, unless you use math-comp

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:06):

and math-comp is not accessible

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:06):

still works

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:06):

10 years after, FT remain state-of-the-art

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:06):

and papers written in 2009 could have been written today

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:06):

so for sure I'm interested in fixing the accessibilty problem

Pierre-Marie Pédrot (Feb 21 2022 at 15:06):

? Lean people are precisely not using a mathcomp style?

Hanneli Tavante (Feb 21 2022 at 15:06):

Possibly unpopular (?) suggestion: What about a simple example (just as in the Lean tutorial) such as commutativity of addition? Then have links for other functionalities

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:06):

pretty close to it

Shachar Itzhaky (Feb 21 2022 at 15:11):

I think properties of lists is pretty canonical for Coq and does not need math-comp (it is not real math heh)

Théo Zimmermann (Feb 21 2022 at 15:12):

Emilio Jesús Gallego Arias said:

"That's precisely the problem, we don't want to teach that to beginners" Lean is doing that and see how Lean vs Coq for the mathematicians is working

Lean arrives years after Coq, teaches to beginners, uses an accessible style, and builds in just a couple of years a library that surpasses the size of MathComp (but according to @Cyril Cohen, this is not going to scale).

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:13):

Indeed, because first thing is that IMVHO, people don't grasp the complexity of the FT proof, so many design chocies that happned in math-comp are actually there for strong reasons!

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:13):

where math-comp failed is in being too focused on qed

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:13):

and other factors

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:13):

political problems were also a strong factor

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:14):

that led to Coq to lose (co) leadership in the field of formal math

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:14):

you can't do a project of that scale and just worry about the QED

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:14):

but that's somethign we have learnt

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:16):

I do agree that this is my own very personal view

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:16):

but I have been programming from a long time

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:16):

and I never liked when I was exposed to style that I thought bad when learning a new system

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:16):

that made me lose interest instantly

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:17):

a proof of the infinitude of primes that takes 200 lines?

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:17):

I immediately don't want to learn more about that language

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:17):

not for me

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:17):

as a programmer I enjoy, even as a beginner, being impressed

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:17):

with stuff that makes me wonder "wow how the hell they are doing that, looks crazy"

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:17):

like when 25 years ago I saw haskell

Théo Zimmermann (Feb 21 2022 at 15:19):

I guess that makes sense, but I don't know how universal this is.

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:19):

Yeah that's why I'm giving the talk

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:19):

to get feedback, etc...

Théo Zimmermann (Feb 21 2022 at 15:19):

Especially if we are looking to expand our reach beyond hackers.

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:19):

I could of course be very wrong

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:20):

For mathematicians I only have a sample size of 2 (direct)

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:20):

but once they got it, they were enjoying it quite well

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:20):

and surprised

Hanneli Tavante (Feb 21 2022 at 15:20):

Opinion: A single example hardly works for everyone, I think. As discussed somewhere https://coq.zulipchat.com/#narrow/stream/314095-Coq-Hackathon.20and.20Working.20Group.2C.20Winter.202022/topic/Coq.20wiki.20getting.20started.20section , wouldn't it be more effective to have different examples according to the audience?

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:20):

both interns

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:20):

Hanneli Tavante said:

Opinion: A single example hardly works for everyone, I think. As discussed somewhere https://coq.zulipchat.com/#narrow/stream/314095-Coq-Hackathon.20and.20Working.20Group.2C.20Winter.202022/topic/Coq.20wiki.20getting.20started.20section , wouldn't it be more effective to have different examples according to the audience?

yes @Hanneli Tavante , I think that's the idea

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:20):

the landing page should be more like an index page

Hanneli Tavante (Feb 21 2022 at 15:24):

Also, some other thoughts:
Who is going to see this landing page?

If you are visiting the page and you never used Coq, how can you make a distinction between what is good and bad style? (Isn't it subjective too? This is a hard question...)
If you are a total beginner, you probably want to get a general sense of what you can do with Coq
If you are an exp. user who needs a quick space to try out some proofs, you might have your own standards.

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:24):

Emilio Jesús Gallego Arias said:

but once they got it, they were enjoying it quite well

everybody seems worried about the syntax, but let me ask you all folks, where's Coq's Kevin Buzzard?

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:24):

_nowhere to be found_

Emilio Jesús Gallego Arias (Feb 21 2022 at 15:24):

Hanneli Tavante said:

Also, some other thoughts:
Who is going to see this landing page?

If you are visiting the page and you never used Coq, how can you make a distinction between what is good and bad style? (Isn't it subjective too? This is a hard question...)

If you are a total beginner, you probably want to get a general sense of what you can do with Coq

If you are an exp. user who needs a quick space to try out some proofs, you might have your own standards.

That sounds very good Hanneli, please add it to the wiki under the "Landing page session" entry

Yves Bertot (Mar 08 2022 at 12:35):

I wanted to develop my own example page, mixing rich text, images, Coq excerpts. Is there a quick route to this? I did not find an edit button on the landing page that would allow me to edit just this page and save it at a place of my choice.

Emilio Jesús Gallego Arias (Mar 08 2022 at 13:40):

Yves for now you need to use coqdoc, or write html by hand

Emilio Jesús Gallego Arias (Mar 08 2022 at 13:40):

What you want is planned and hopefully to land in time for the Coq workshop submission

Emilio Jesús Gallego Arias (Mar 08 2022 at 13:41):

If someone would like to help hacking I could actually guide them in the implementation, myself I got no hacking time until the 17th

Emilio Jesús Gallego Arias (Mar 08 2022 at 13:41):

but then I got lots, finally!

Shachar Itzhaky (Mar 08 2022 at 20:50):

It reminds me that we have to take another look at Alectryon as a doc system that supports markdown together with Coq-related features; this can be useful for literate document editing as well as the jsCoq wiki.

Emilio Jesús Gallego Arias (Mar 08 2022 at 20:50):

Indeed I hope to chat to @Clément Pit-Claudel tomorrow a bit

Emilio Jesús Gallego Arias (Mar 08 2022 at 20:50):

maybe you would like to join?

Shachar Itzhaky (Mar 08 2022 at 20:51):

Nice!! I do have some time tomorrow. What time?

Emilio Jesús Gallego Arias (Mar 08 2022 at 21:04):

Clément said 5pm , I proposed 6pm

Emilio Jesús Gallego Arias (Mar 08 2022 at 21:05):

both work for me so 5 pm is also good

Emilio Jesús Gallego Arias (Mar 08 2022 at 21:05):

tho I prefer later if possible

Emilio Jesús Gallego Arias (Mar 08 2022 at 21:05):

Paris time, I'm talking about

Shachar Itzhaky (Mar 08 2022 at 21:40):

5p Paris is good for me as well. I can also do later. Let me know.

Emilio Jesús Gallego Arias (Mar 08 2022 at 21:47):

Great

Emilio Jesús Gallego Arias (Mar 08 2022 at 21:52):

I've sent a mail, we can sync offline

Last updated: May 31 2023 at 02:31 UTC