Zulip Chat Archive

Stream: general

Topic: reStructured Text and Lean


Simon Hudon (Jun 18 2018 at 01:49):

I'm looking at the build system of https://github.com/leanprover/theorem_proving_in_lean to adapt Software Foundations and I can't find where the html and latex lean syntax highlighting is defined. Can someone give me a hint?

Andrew Ashworth (Jun 18 2018 at 02:49):

It's a custom fork of pygments... has it disappeared from the repo?

Simon Hudon (Jun 18 2018 at 02:50):

It is still working, I just couldn't figure out how to update the syntax (e.g. def instead of definition)

Simon Hudon (Jun 18 2018 at 02:53):

Oh I see that Pygment is referred to in the Makefile. That's pretty much the only place I see it

Andrew Ashworth (Jun 18 2018 at 02:54):

Did you recursively clone git submodules?

Simon Hudon (Jun 18 2018 at 02:55):

The submodule list seems empty

Andrew Ashworth (Jun 18 2018 at 02:56):

As an aside, I remember chatting briefly about SF and lean a month ago. I made some progress but I'm slow since it's a weekend thing. If you want to take it up let me know if there's some part I can take care of

Andrew Ashworth (Jun 18 2018 at 02:56):

Hmm, I'm not at my workstation to see how I handled pygments

Simon Hudon (Jun 18 2018 at 02:57):

Did you set everything up already?

Andrew Ashworth (Jun 18 2018 at 02:58):

I have a skeleton project, yes

Simon Hudon (Jun 18 2018 at 02:58):

Would you care to share it with me. It might be better than starting over :D

Andrew Ashworth (Jun 18 2018 at 02:59):

Sure, but I can't get to it until tomorrow, unfortunately

Andrew Ashworth (Jun 18 2018 at 03:00):

Feel free to remind me tomorrow if I forget :)

Simon Hudon (Jun 18 2018 at 03:00):

It might be best: it's write-o-clock right now (thesis time) so it's best if I have a reason to drop it

Simon Hudon (Jun 18 2018 at 03:01):

Very well, I will :D

Gabriel Ebner (Jun 18 2018 at 07:21):

Yes, the Lean 3 syntax highlight is not upstream yet. The makefile installs my fork https://bitbucket.org/gebner/pygments-main/src into a venv.

Kevin Buzzard (Jun 18 2018 at 07:43):

As an aside, I remember chatting briefly about SF and lean a month ago. I made some progress but I'm slow since it's a weekend thing. If you want to take it up let me know if there's some part I can take care of

My son will be taking this on in early July as part of a work experience project.

Kevin Buzzard (Jun 18 2018 at 07:44):

Only one week and he's learning as he goes so he probably won't do so much.

Kevin Buzzard (Jun 18 2018 at 07:46):

If you've set it up so he could write in rst and it looked beautiful I bet he would oblige. I will probably push him to write it in rst anyway, I've been writing my book in rst using the sphinx lean extension that I took from the TPIL repo and I'm really happy with the results.

Kevin Buzzard (Jun 18 2018 at 07:47):

But he'll have to start from the beginning when it comes to the Coq

Simon Hudon (Jun 19 2018 at 15:11):

I talked to Benjamin Pierce and he's pretty happy that we want to make a Lean version. If we want, we could work off of the SF sources but we'd have to donate the copyrights of our contribution. Otherwise, if we're happy to work with the html, we're free to do as we please

Simon Hudon (Jun 19 2018 at 15:14):

I'm actually on the fence about this decision. Because we use the same template as Theorem Proving in Lean, it seems sufficient to only use the html code. But at the same time, it would be great if we could synchronize the evolution of SF-lean with the evolution of the original

Andrew Ashworth (Jun 22 2018 at 06:02):

I feel guilty about publishing this template since it's quite unpolished, but...

Andrew Ashworth (Jun 22 2018 at 06:02):

@Simon Hudon https://github.com/alashworth/sf-lean

Andrew Ashworth (Jun 22 2018 at 06:02):

An example of what it looks like on GH-Pages: https://alashworth.github.io/sf-lean/vol1/basics.html

Andrew Ashworth (Jun 22 2018 at 06:03):

To compile, first set up a virtual python environment, and then issue pip install https://bitbucket.org/gebner/pygments-main/get/default.tar.gz#egg=Pygments

Andrew Ashworth (Jun 22 2018 at 06:03):

this is in addition to the Sphinx dependency...

Andrew Ashworth (Jun 22 2018 at 06:13):

This is my first time using Sphinx for documentation... actually, it's pretty nice. When Lean 4 rolls around, maybe I'll take a look at adding a Lean domain.

Simon Hudon (Jun 22 2018 at 15:56):

I'm not fond of working with Python but once it works, it's a nice template

Simon Hudon (Jun 22 2018 at 15:57):

I suggest we setup a travis build and a status for each chapters: adapted text / adapted code / needs review

Andrew Ashworth (Jun 22 2018 at 17:49):

How do you want to handle exercises? Sorry them out as in the original text or have solutions?

Andrew Ashworth (Jun 22 2018 at 17:50):

I'm inclined to having solutions in the text, as this resource will mostly be for self-learners as opposed to a classroom with homework

Simon Hudon (Jun 22 2018 at 17:52):

That's makes sense. However, Benjamin Pierce did request that no exercise solution be posted online. I'd like to see how we can reconcile both goals. Maybe we can hand some solutions out upon request

Andrew Ashworth (Jun 22 2018 at 17:52):

I'll see what I can do regarding travis and others this weekend, then. I wasn't sure if you wanted to fork and work on it yourself or not

Simon Hudon (Jun 22 2018 at 17:52):

I think we could organize around a single repo. At least for now

Andrew Ashworth (Jun 22 2018 at 17:53):

I understand he didn't want solutions online, but 1) it's Lean, not Coq, and 2) solutions are already on Github...

Simon Hudon (Jun 22 2018 at 18:01):

2) if we're the official lean-SF version, we'd be endorsing doing the opposite of what the authors requested. That's different

Simon Hudon (Jun 22 2018 at 18:03):

1) Lean is close enough to Coq that we can translate a Coq book into Lean ...

Johan Commelin (Jun 22 2018 at 18:04):

Suppose that at some point we have a tactic that is able to solve all these exercises... does that mean that this tactic must not be published online?

Simon Hudon (Jun 22 2018 at 18:05):

No, what it would mean is let's not publish it as a solution to the SF exercises

Andrew Ashworth (Jun 22 2018 at 18:05):

It just personally bums me out when solutions aren't given out with a text

Andrew Ashworth (Jun 22 2018 at 18:06):

SF doesn't even give out solutions to odd-numbered exercises or anything like that

Andrew Ashworth (Jun 22 2018 at 18:17):

well, at the end of the day, there's a whole lot of work to be done before this even becomes an issue

Simon Hudon (Jun 22 2018 at 18:18):

That's true

Simon Hudon (Jun 22 2018 at 18:18):

I agree with the need for self-study

Simon Hudon (Jun 22 2018 at 18:18):

I think we should also respect the wishes of the authors

Simon Hudon (Jun 22 2018 at 18:19):

I wonder if there's a way of reconciling both

Andrew Ashworth (Jun 22 2018 at 18:19):

Perhaps we can come up with similar exercises that are "different enough"

Andrew Ashworth (Jun 22 2018 at 18:20):

honestly after having worked through some, the solutions are in the implementation sense pretty different

Andrew Ashworth (Jun 22 2018 at 18:20):

Lean really encourages you to use the equation compiler instead of match

Andrew Ashworth (Jun 22 2018 at 18:20):

lots of the lemmas regarding lists are subtly different

Simon Hudon (Jun 22 2018 at 18:20):

That could be an approach. The other thing might be, if it comes to be useful in the classroom, the instructor set might include a variation on the exercises in the book with solutions that we communicate with instructors only

Simon Hudon (Jun 22 2018 at 18:22):

We can keep that issue open. In the mean time, what do you think of it if we ask Pierce to weigh in. We can show him our exercises and solutions and ask him if they are different enough

Andrew Ashworth (Jun 22 2018 at 18:22):

Yep. Let's wait until everything but the exercises is done though... hah. I don't want to show this off in its current state

Simon Hudon (Jun 22 2018 at 18:25):

Fair enough :) I think if courageous users want to try it out while we work, it would be great to get bug reports.

Simon Hudon (Jun 22 2018 at 18:53):

Btw, would you mind giving me commit rights to that repo, I'll start structuring things.

Andrew Ashworth (Jun 22 2018 at 19:00):

sure, sent you a link. the paths definitely need cleaning up, maybe everything under /src should go to /src/vol1 for consistency... the source file link is broken in the GH-Pages build

Simon Hudon (Jun 22 2018 at 19:03):

Thanks!

Simon Hudon (Jun 22 2018 at 19:05):

There's a program for encrypted git repos, it's called Keybase. We may want to put the solutions there

Simon Hudon (Jun 22 2018 at 19:12):

Instead of publishing solutions, we may want to dedicate a channel where it's ok to discuss solutions. It might make it easier to give help to people studying the material without broadcasting the solutions

Simon Hudon (Jun 22 2018 at 21:57):

You seem to have taken out all the links to Lean live. Don't you want that connection? That would make it easier to follow the book online, no?

Andrew Ashworth (Jun 22 2018 at 22:04):

It wasn't deliberate, I was just too lazy to figure out how the lean-sphinx script worked

Andrew Ashworth (Jun 22 2018 at 22:06):

also on the todo list: write up a readme that uses elan for a seamless newbie experience

Andrew Ashworth (Jun 22 2018 at 22:09):

these things are on the bottom of my priority list though, I think translating the content is the first step

Simon Hudon (Jun 22 2018 at 22:12):

Ah good to know! I've been hacking at the scripts this week so I'll just bring my stuff over

Simon Hudon (Jun 22 2018 at 22:17):

How is this for a start?

Simon Hudon (Jun 22 2018 at 22:17):

https://github.com/alashworth/sf-lean

Andrew Ashworth (Jun 22 2018 at 22:23):

sounds reasonable and is what i was planning on doing

Simon Hudon (Jun 23 2018 at 20:46):

I'm going to keep working on basics.rst and basics.lean. I think we should checkin with the sections we work on. Conflicts seems much more likely on a project like this.

Simon Hudon (Jun 23 2018 at 21:35):

@Andrew Ashworth when you have a moment can you enable travis build for your repo. I'm about to commit a travis configuration. We just need to link the account with a travis account

Andrew Ashworth (Jun 23 2018 at 22:31):

ugh, I tried to get it working with travis-ci.com since travis-ci.org is deprecated, but apparently I managed to set the repo up on travis-ci.org accidentally, and migrations have to be done manually by travis support

Andrew Ashworth (Jun 23 2018 at 22:31):

so... I'm waiting to hear back from their account management team

Simon Hudon (Jun 23 2018 at 22:33):

I wasn't aware travis-ci.org was deprecated. Does that mean anything for their support for open source projects?

Andrew Ashworth (Jun 23 2018 at 22:33):

no, still free, the point is travis wants to unify their commercial and open source together on the same domain (the .com)

Andrew Ashworth (Jun 23 2018 at 22:34):

github has marked the legacy travis service as deprecated as well

Simon Hudon (Jun 23 2018 at 22:40):

I wonder if we'll see a difference

Simon Hudon (Jun 23 2018 at 22:42):

For the snippets, I'm thinking of loading the complete lean file of the current chapter when you click on try it. There's so much continuity that you can't just load them in isolation

Simon Hudon (Jun 23 2018 at 22:42):

But I don't like that you'd get that much code to look at when you click try it

Andrew Ashworth (Jun 23 2018 at 22:43):

that's also the problem with try it

Andrew Ashworth (Jun 23 2018 at 22:43):

another reason i didn't spend too much time trying to get it to work

Andrew Ashworth (Jun 23 2018 at 22:44):

chapters 1-5 are cumulative

Simon Hudon (Jun 23 2018 at 22:45):

I wonder if we could get local files into the live Lean version and just do an import

Simon Hudon (Jun 23 2018 at 22:46):

I think those chapters are where the live version would be most profitable

Andrew Ashworth (Jun 23 2018 at 22:51):

I personally don't see a lot of value in lean.js, the coding experience is far below vscode or emacs

Andrew Ashworth (Jun 23 2018 at 22:51):

sf is sufficiently complicated, and elan so easy to use, hopefully....

Andrew Ashworth (Jun 23 2018 at 22:52):

I expect a programmer learning from SF to be able to set up a minimal dev environment? idk

Simon Hudon (Jun 23 2018 at 22:54):

Those things are true. I think it helps get you started quicker. If I have to set up a new environment, even when people tell me it will take only a few seconds, I expect I'll have to set aside a few hours so I don't get started until I'm ready to put those hours. If the online version is there, it acts as an argument that it is worth putting the time. Then it comes as a surprise that it actually doesn't take any time

Andrew Ashworth (Jun 23 2018 at 22:55):

in addition, apparently there will be a Lean dev environment available on CoCalc at some point

Simon Hudon (Jun 23 2018 at 22:56):

I'll have to see that

Simon Hudon (Jun 23 2018 at 22:57):

Btw, I really like what you did with

.. literalinclude:: ../../src/basics.lean
  :language: lean
  :start-at: inductive day : Type
  :end-at: saturday

It might become my favorite way of doing literate programming

Andrew Ashworth (Jun 23 2018 at 22:58):

i noticed you changed up conf.py. I need to figure out how to add the source directory to the sphinx path

Andrew Ashworth (Jun 23 2018 at 22:58):

ahh, maybe tomorrow

Simon Hudon (Jun 23 2018 at 22:58):

Haha :) Sorry, it was pretty draconian. We can sit down together to mitigate the damage

Simon Hudon (Jun 23 2018 at 22:58):

Anyway, food is calling to me

Andrew Ashworth (Jun 23 2018 at 22:59):

np! enjoy dinner

Simon Hudon (Jun 23 2018 at 23:01):

Thanks!

Andrew Ashworth (Jun 23 2018 at 23:13):

Btw, I really like what you did with

.. literalinclude:: ../../src/basics.lean
  :language: lean
  :start-at: inductive day : Type
  :end-at: saturday

It might become my favorite way of doing literate programming

I'm not a huge fan of Sphinx's ability to match strings. I don't understand how it works, and it often fails for me

Andrew Ashworth (Jun 23 2018 at 23:15):

so much so that when I was writing that basics.rst snippet I had a text editor on one screen and a terminal + chrome window on the other so I could do a terrible version of live preview

Simon Hudon (Jun 24 2018 at 00:24):

Do you use emacs or VS code?

Simon Hudon (Jun 24 2018 at 00:47):

Also, how do you update your gh-pages?

Andrew Ashworth (Jun 24 2018 at 01:44):

the old fashioned way: cut and paste

Andrew Ashworth (Jun 24 2018 at 01:44):

if you want to script it, you could try using https://github.com/davisp/ghp-import, which is on my 'to-investigate' list

Simon Hudon (Jun 24 2018 at 02:01):

So if I play the elaborator, you compile the rst files and copy all the html files in vol1 and then commit that

Andrew Ashworth (Jun 24 2018 at 02:04):

at project root, issue make html, then copy build/html to the root dir, and commit this to the gh-pages branch

Simon Hudon (Jun 24 2018 at 02:05):

Even better! Thanks!

Andrew Ashworth (Jun 24 2018 at 02:05):

this is with my version of conf.py, I haven't checked if TPIL's conf.py does things differently

Simon Hudon (Jun 24 2018 at 02:05):

When it comes to the web, I'm kind of an ignoramus

Andrew Ashworth (Jun 24 2018 at 02:07):

yeah, I'm not a web programmer either... I think I know just enough to be dangerous

Simon Hudon (Jun 24 2018 at 02:14):

Haha :D that's still more than me

Andrew Ashworth (Jun 24 2018 at 03:07):

can you go into more detail about the def issue you just raised? https://alashworth.github.io/sf-lean/vol1/basics.html - def is colored green for me

Andrew Ashworth (Jun 24 2018 at 03:08):

@Simon Hudon

Simon Hudon (Jun 24 2018 at 03:08):

Interesting, it doesn't get colored for me. Maybe we have inconsistent stylesheets?

Andrew Ashworth (Jun 24 2018 at 03:09):

so when you navigate to that page, def isn't highlighted?

Simon Hudon (Jun 24 2018 at 03:14):

Exactly

Simon Hudon (Jun 24 2018 at 03:14):

Have a look at:

https://alashworth.github.io/sf-lean/vol1/basics.html#

Simon Hudon (Jun 24 2018 at 03:14):

(btw, feel free to criticize the end of the Numbers section. I had to take some creative freedom)

Andrew Ashworth (Jun 24 2018 at 03:16):

yeah, i'm looking at it

Andrew Ashworth (Jun 24 2018 at 03:16):

Andrew Ashworth (Jun 24 2018 at 03:16):

is this what it looks like for you? if not, I think something is up on your end

Andrew Ashworth (Jun 24 2018 at 03:17):

oh

Andrew Ashworth (Jun 24 2018 at 03:17):

you pushed something new

Simon Hudon (Jun 24 2018 at 03:17):

I think you should refresh. I just updated it

Andrew Ashworth (Jun 24 2018 at 03:18):

if it's only def, the likely reason is that you have conflicting versions of pygments installed

Andrew Ashworth (Jun 24 2018 at 03:18):

then when you compile, the html isn't getting styled correctly as a result

Simon Hudon (Jun 24 2018 at 03:21):

How do I fix that?

Andrew Ashworth (Jun 24 2018 at 03:22):

pip uninstall pygments

Andrew Ashworth (Jun 24 2018 at 03:23):

then reinstall from the pygments fork

Simon Hudon (Jun 24 2018 at 03:29):

It worked like a charm! Thanks :)

Andrew Ashworth (Jun 24 2018 at 03:30):

np

Simon Hudon (Jun 24 2018 at 03:30):

Btw: I decided to take the lazy way for publishing and I did git init in build/html and added gh-pages as a remote. It doesn't seem too bad

Andrew Ashworth (Jun 24 2018 at 03:31):

yep, i bet that would work too

Andrew Ashworth (Jun 24 2018 at 03:32):

that is actually lazier than cut and paste... wish i'd done that first

Simon Hudon (Jun 24 2018 at 03:35):

I work pretty hard to be this lazy :stuck_out_tongue_closed_eyes:

Simon Hudon (Jun 24 2018 at 03:37):

It should look better now at https://alashworth.github.io/sf-lean/vol1/basics.html#

Andrew Ashworth (Jun 24 2018 at 03:38):

hmm, the try it hyperlink overlaps code

Simon Hudon (Jun 24 2018 at 03:39):

Which one?

Andrew Ashworth (Jun 24 2018 at 03:39):

all the one liner defs and examples

Andrew Ashworth (Jun 24 2018 at 03:40):

for example, example : next_weekday (next_weekday day...

Simon Hudon (Jun 24 2018 at 03:41):

Ah! Do you mean that it displays "try it" on top of the code? I thought somehow snippets got mixed up when sent to Lean Live

Andrew Ashworth (Jun 24 2018 at 03:42):

the way the try it works with snippets is not very suitable to how SF is currently laid out

Andrew Ashworth (Jun 24 2018 at 03:42):

for example, none of the nat playground stuff works because the namespace command isn't sent to lean.js

Andrew Ashworth (Jun 24 2018 at 03:43):

i would like to revert conf.py until one of us has time to really sit down and make it work correctly.

Simon Hudon (Jun 24 2018 at 03:43):

The snippets have a lot of problems. I'd like to send the whole file over

Simon Hudon (Jun 24 2018 at 03:43):

Sure. What does your version do?

Andrew Ashworth (Jun 24 2018 at 03:43):

no "try it" at all

Simon Hudon (Jun 24 2018 at 03:44):

I could work on the "try it" in a branch until I get it right

Andrew Ashworth (Jun 24 2018 at 03:44):

to make it work correctly, we need to build lean live with our own lean source files

Andrew Ashworth (Jun 24 2018 at 03:44):

and we also need some way to send a scroll command

Andrew Ashworth (Jun 24 2018 at 03:44):

or embed a line position in the hyperlink

Andrew Ashworth (Jun 24 2018 at 03:45):

if we do want to have a web link

Simon Hudon (Jun 24 2018 at 03:45):

That would be good, you're right.

Andrew Ashworth (Jun 24 2018 at 03:45):

then we should perhaps link the whole source file at the top of the chapter

Andrew Ashworth (Jun 24 2018 at 03:45):

and ask people to scroll down as they read

Andrew Ashworth (Jun 24 2018 at 03:45):

that's the low-effort way

Simon Hudon (Jun 24 2018 at 03:45):

Maybe we can recruit @Gabriel Ebner or @Sebastian Ullrich to help us with that

Simon Hudon (Jun 24 2018 at 03:46):

Yeah, and then the link can bring up Lean Live at the right line number

Andrew Ashworth (Jun 24 2018 at 03:48):

yeah, i think for now it would be best to work on it in its own branch

Andrew Ashworth (Jun 24 2018 at 03:51):

TPIL does some trickery with selectively hiding lines

Kevin Buzzard (Jun 24 2018 at 09:52):

So this all looks really good -- both nice to look at, and great material. Is it really not an issue that the text is basically all lifted from someone else's work? If not then that's awesome. My son will be starting on doing the exercises on Monday 2nd July, he is a beginner but he's a decent python programmer and is hopefully smart enough to learn quickly (and I can help him of course). I was going to advise him to just read SF in the original Coq and I was going to help him translate, but if he can read the translated stuff that would be awesome. I have done many of the exercises of Part 1 in Lean myself and I will have the answers somewhere -- I did them once I knew a lot about how Lean worked so they weren't too much trouble.

Simon Hudon (Jun 24 2018 at 13:44):

Great! And please send us comments as you go if there are parts that don't quite add up.

Is it really not an issue that the text is basically all lifted from someone else's work?

Not an issue. The html version of the book is under MIT license and I talked to the author. He seems pretty happy that we're doing that and had great information on how to proceed.

Simon Hudon (Jun 24 2018 at 13:46):

(comments or even contribution to the text)

Simon Hudon (Jun 24 2018 at 15:42):

@Andrew Ashworth What was the reason for you to use to specify lean snippets in a single Lean file instead of inline in the rst file? I'm thinking it might be easier to write this way, especially considering that the flow of the chapter pretty much follows the declaration flow.

Andrew Ashworth (Jun 24 2018 at 15:54):

later in the book we will want to use leanpkg to manage dependencies on cooper and mathlib

Andrew Ashworth (Jun 24 2018 at 15:55):

the more involved exercises use a lot of omega

Simon Hudon (Jun 24 2018 at 15:56):

I thought we could use a make file to first generate the Lean sources and then call leanpkg

Simon Hudon (Jun 24 2018 at 15:57):

The biggest downside I see is with debugging the Lean code

Andrew Ashworth (Jun 24 2018 at 16:02):

i think a common way to interact with the textbook will be for people to clone the repository and step through the source files themselves

Andrew Ashworth (Jun 24 2018 at 16:02):

you can't work with the .rst file like a .lean file

Simon Hudon (Jun 24 2018 at 16:03):

That's true. I'd really like for there to be a literate mode to Lean

Simon Hudon (Jun 24 2018 at 16:04):

I think we can offer a similar experience though by building an archive file that people can download. And in that file, we put the Lean generate files and the rst files, to follow along.

Andrew Ashworth (Jun 24 2018 at 16:06):

i can't comment on this approach since I don't know how the TPIL lean-sphinx node parsing code works

Simon Hudon (Jun 24 2018 at 16:07):

I think that's feasible. Remains to see if it's a workflow we're comfortable with

Andrew Ashworth (Jun 24 2018 at 16:08):

from a gut feeling perspective, it feels backwards to me. If I had unlimited time, I would write a Lean plugin for sphinx so we could move even more comments and documentation into the .lean files

Simon Hudon (Jun 24 2018 at 16:11):

Yeah, I'd love that

Andrew Ashworth (Jun 24 2018 at 16:11):

from a teaching perspective, I think it's nice if the project demonstrates how to manage a larger Lean development

Simon Hudon (Jun 24 2018 at 16:11):

I've been asking for a literate mode for a while. Maybe Lean 4 will make it easier to do ...

Andrew Ashworth (Jun 24 2018 at 16:12):

the inline code approach with snippets is attractive because it enables us to reuse all the scripts from TPIL, and in particular maybe make it easier to enable 'try it'

Andrew Ashworth (Jun 24 2018 at 16:12):

well, you already know how I feel about how useful that functionality is

Simon Hudon (Jun 24 2018 at 16:13):

Are you referring to a previous conversation ... I only have vague memories of that. You weren't too favorable to the idea, were you?

Andrew Ashworth (Jun 24 2018 at 16:13):

well, to recap, I think it's a big hassle for us to make it work correctly

Simon Hudon (Jun 24 2018 at 16:14):

For us the users?

Andrew Ashworth (Jun 24 2018 at 16:14):

for us, the authors

Andrew Ashworth (Jun 24 2018 at 16:14):

and also nobody is going to want to be doing the more involved exercises in lean.js

Andrew Ashworth (Jun 24 2018 at 16:16):

I think between elan and a possible Lean environment being set up on co-calc, its not a good use of time to try and get it to work, when there's so much translation effort to be done

Simon Hudon (Jun 24 2018 at 16:16):

I think you misunderstood my point about literate programming. The point is to have the html and pdf generated from a Lean file, the prose is considered as comment when compiling so you don't have to maintain two separate sets of files when writing tutorials or blogs or books

Andrew Ashworth (Jun 24 2018 at 16:17):

if you want something similar to coqtop

Andrew Ashworth (Jun 24 2018 at 16:17):

a Sphinx plugin would do that

Andrew Ashworth (Jun 24 2018 at 16:17):

it could be written today

Andrew Ashworth (Jun 24 2018 at 16:18):

but that doesn't help you when you want to discuss things out of the order they are defined in the source

Andrew Ashworth (Jun 24 2018 at 16:19):

then i think the way sf-lean is currently structured is the best

Simon Hudon (Jun 24 2018 at 16:42):

That's something I've been arguing for as well. If lean provided a declaration like postpone my_foo your_foo their_foo then that could allow you to make small breaks in the declaration order.

Jesse Michael Han (Jun 25 2018 at 15:42):

it'd be nice also if extracted Lean snippets (a la TPIL) could refer to/import each other---this is something that'll come up sooner or later in the formal abstracts project, since there'll be theorems we want to formally state that require other definitions/theorems that only exist as formal abstract snippets

Simon Hudon (Jun 25 2018 at 15:48):

I'm not too familiar with the formal abstracts project. Do you mean that you'd like in Lean Live to import
chapters of TPIL?

Jesse Michael Han (Jun 25 2018 at 15:57):

Currently it's organized as a Sphinx project with Gabriel's lean_sphinx extension: https://github.com/thalesant/formalabstracts

I mean that if there's a page for e.g. the continuum hypothesis, containing a code block, then i'd like to be able to import that code block when i write a new page about the independence of the continuum hypothesis

Simon Hudon (Jun 25 2018 at 16:08):

I see so if the whole project was source code would make it easier to use. I agree

Kevin Buzzard (Jul 02 2018 at 08:55):

It should look better now at https://alashworth.github.io/sf-lean/vol1/basics.html#

OK so my son is going to start on the exercises today. Many thanks to both Andrew and Simon for making his life less difficult!

Elliott Macneil (Jul 02 2018 at 10:03):

I'm wondering if someone could possibly direct me to where the source code (the file basic.lean) is, as the link on the website doesn't work

Patrick Massot (Jul 02 2018 at 10:05):

https://github.com/alashworth/sf-lean/blob/lean-3.4.1/src/basics.lean

Elliott Macneil (Jul 02 2018 at 10:06):

Thanks!


Last updated: Dec 20 2023 at 11:08 UTC