talk.tryitonline.net

2:51 AM

@Pavel tio.run/#lean

Thanks!

2 hours later…

4:29 AM

@Dennis I actually... uh... didn't expect this at all lol

ok so Lean comes with a library called mathlib

so you might want to install it in your tio

and another problem is that I would consider Lean and mathlib to be in development

by that I mean it literally updates every two days or so

and as for mathlib, it's even more frequent

I've installed the binaries from the latest release, which is from September '17.

oh ok

are you going to install the library?

Where do I find it?

Ah, separate repo.

github.com/leanprover/mathlib

github.com/leanprover/mathlib/commits

the latest build fails, so you might need to look into the commits history

...and you'll find me committing every few weeks or so

I just added Knaster-Tarski theorem yesterday

How do I install mathlib?

4:35 AM

do you use git?

Yes.

did you use git for Lean?

Ah, sorry. No. I downloaded the latest release.

does it come with lean/bin/leanpkg?

It does.

4:37 AM

Getting the nightly release might? be better

wonderful

@Pavel could you send me a link?

@LeakyNun On the download page

leanprover.github.io/download

There's binaries and nightlies

does that take care of mathlib?

cd /c/
git clone github.com/leanprover/mathlib
cd mathlib
/c/lean/bin/leanpkg build

@Dennis anyway here's the git code I use to download and build mathlib

but you don't want to download HEAD since it doesn't build

so you need to git checkout d84af03 before the last line

user56656

Could purescript be added?

@LeakyNun Still getting a lot of errors. Is master compatible with the latest release or should I be using lean-3.3.0?

Or should I switch to the nightly?

4:47 AM

you should probably switch to the nightly

since your current version is September something

thank you very much for this though

My pleasure. Lean looks quite interesting.

@user56656 I'll take a look. Probably tomorrow.

user56656

No problem. I need to learn purescript before I can start making answers in it.

git checkout lean-3.3.0 works with the release btw. I'll try the nightly now.

5:28 AM

The new mathlib finished building.

How do I test if it is working?

tio.run/##y0lNzPv/…

OK, looks like I have to adjust LEAN_PATH.

What should I set it to? Lean is in /opt/lean.

Or do I just have to move mathlib?

It's currently in /opt/lean/mathlib.

Does it work if you link it to /home/runner

No.

what is lean_path currently?

5:38 AM

I seem to have figured it out.

tio.run/##y0lNzPv/…

nice! what did you do

export LEAN_PATH=/opt/lean/lib/lean/library:/opt/lean/lib/lean/mathlib

thank you very much

Let me know when I should update something.

5:48 AM

Feature request: mathlib nightlies ;)

hmm, I’ll see what I can do

8 hours later…

Conor O'Brien

2:17 PM

@Dennis could you please pull attache?

2:30 PM

@ConorO'Brien Done.

Conor O'Brien

2:42 PM

thanks!

3:14 PM

→ 115 messages moved to Lean

@LeakyNun TIO now automatically builds the latest version of mathlib that was OK'd by Travis.

@Dennis :O

Well, semi-automatically. I still have to initiate the pull myself, but it does git checkout HEAD^ until the current commit has status "success".

I see

thanks a lot

3 hours later…

caird coinheringaahing

6:13 PM

@Dennis FYI, I changed the main branch for Whispers to this, would you mind updating and puling it please?

1 hour later…