Stream: jsCoq

Topic: jsCoq landing page


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

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

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

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

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

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:02):

in terms of proof difficulty,

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:03):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:03):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:03):

I agree math-comp is not accesible

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:04):

but let's move this to the right place please

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:05):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:06):

and math-comp is not accessible

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:06):

still works

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:06):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:06):

and papers written in 2009 could have been written today

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:06):

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

view this post on Zulip Pierre-Marie Pédrot (Feb 21 2022 at 15:06):

? Lean people are precisely not using a mathcomp style?

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:06):

pretty close to it

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:13):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:13):

and other factors

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:13):

political problems were also a strong factor

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:14):

but that's somethign we have learnt

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:16):

I do agree that this is my own very personal view

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:16):

but I have been programming from a long time

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:16):

that made me lose interest instantly

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:17):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:17):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:17):

not for me

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:17):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:17):

like when 25 years ago I saw haskell

view this post on Zulip Théo Zimmermann (Feb 21 2022 at 15:19):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:19):

Yeah that's why I'm giving the talk

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:19):

to get feedback, etc...

view this post on Zulip Théo Zimmermann (Feb 21 2022 at 15:19):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:19):

I could of course be very wrong

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:20):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:20):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:20):

and surprised

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:20):

both interns

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:20):

the landing page should be more like an index page

view this post on Zulip Hanneli Tavante (Feb 21 2022 at 15:24):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 15:24):

_nowhere to be found_

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 13:40):

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 13:41):

but then I got lots, finally!

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 20:50):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 20:50):

maybe you would like to join?

view this post on Zulip Shachar Itzhaky (Mar 08 2022 at 20:51):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:04):

Clément said 5pm , I proposed 6pm

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:05):

both work for me so 5 pm is also good

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:05):

tho I prefer later if possible

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:05):

Paris time, I'm talking about

view this post on Zulip Shachar Itzhaky (Mar 08 2022 at 21:40):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:47):

Great

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2022 at 21:52):

I've sent a mail, we can sync offline


Last updated: Jan 31 2023 at 09:01 UTC