Zulip Chat Archive

import system.io data.buffer.parser data.int.basic
open tactic parser

def number : parser ℕ :=
string.to_nat <$> many_char1 (sat $ λ c,
  '0'.to_nat ≤ c.to_nat ∧ c.to_nat ≤ '9'.to_nat)

def signed_number : parser ℤ :=
ch '+' >> (int.of_nat <$> number) <|>
ch '-' >> ((λ x:ℕ, -x) <$> number)

run_cmd do
  s ← tactic.unsafe_run_io $ io.fs.read_file "dat.txt",
  sum.inr l ← return $ run (many (signed_number <* ch '\n')) s,
  trace l

[13,
 -(2+1),
 -(7+1),
 14,
 16,
 -(6+1),
 3,
 -(6+1),
 9,
 -(9+1),
 16,
...

Mario Carneiro (Dec 01 2018 at 13:59):

maybe @Sebastian Ullrich knows the correct way to call IO from run_cmd, but unsafe_run_io works in a pinch

Sebastian Ullrich (Dec 01 2018 at 14:00):

I think you can use #eval

Mario Carneiro (Dec 01 2018 at 14:03):

oh, I should have used to_string, the output is much nicer

import system.io data.buffer.parser
open parser

def number : parser ℕ :=
string.to_nat <$> many_char1 (sat $ λ c,
  '0'.to_nat ≤ c.to_nat ∧ c.to_nat ≤ '9'.to_nat)

def signed_number : parser ℤ :=
ch '+' >> (int.of_nat <$> number) <|>
ch '-' >> ((λ x:ℕ, -x) <$> number)

#eval do
  s ← io.fs.read_file "dat.txt",
  sum.inr l ← return $ run (many (signed_number <* ch '\n')) s,
  trace (to_string l) (return ())

[13, -3, -8, 14, 16, -7, 3, -7, 9, -10, 16, 13, 12, 12, 4, 19, -2, -5, -15, -2, -13, -11, -13, -2, ...

Mario Carneiro (Dec 01 2018 at 14:05):

For some reason the output or return value of the io is ignored, so I had to to a hack with trace to get it to print

Patrick Massot (Dec 01 2018 at 14:10):

Thanks Mario! It allowed to complete Day 1, adding only 15 characters to your code :)

Edward Ayers (Dec 01 2018 at 14:12):

Did you do the second part?

Mario Carneiro (Dec 01 2018 at 14:27):

here's how I did the first part in lean:

#eval 0
+13
-3
-8
+14
+16

Patrick Massot (Dec 01 2018 at 14:52):

No, I decided I should stop distractions for a while. And also the question looked masochistic to do in functional rather than imperative language

Patrick Massot (Dec 01 2018 at 14:53):

Mario, was that all your input?

Bryan Gin-ge Chen (Dec 01 2018 at 15:49):

I had to use #eval (0 : int) since the first line of the input was negative.

Reid Barton (Dec 02 2018 at 00:54):

I solved it too. But my solution took 40 seconds to run

Reid Barton (Dec 02 2018 at 00:55):

The first part, I mean

Reid Barton (Dec 02 2018 at 01:06):

Doing the second part in non-meta Lean seems pretty interesting

Mario Carneiro (Dec 02 2018 at 08:17):

I think this is a good test case for the conventional programming capabilities of lean. Here's my solution for day 2 pt 1:

import system.io data.buffer.parser meta.rb_map data.list.basic
open parser

def letter : parser char :=
sat (λ c, 'a'.to_nat ≤ c.to_nat ∧ c.to_nat ≤ 'z'.to_nat)

def count1 {α lt} [decidable_rel lt] (c : rbmap α ℕ lt) (a : α) : rbmap α ℕ lt :=
c.insert a $ match c.find a with
| (some n) := n + 1
| none := 1
end

def get_counts (l : list char) : bool × bool :=
let m := list.foldl count1 (mk_rbmap char ℕ) l in
m.fold (λ c n ⟨r₁, r₂⟩, ⟨r₁ ∨ n = 2, r₂ ∨ n = 3⟩) (ff, ff)

#eval do
  s ← io.fs.read_file "dat.txt",
  sum.inr ls ← return $ run (many (many letter <* ch '\n')) s,
  let (l₁, l₂) := (ls.map get_counts).unzip,
  trace (to_string (l₁.count tt * l₂.count tt)) (return ())

Mario Carneiro (Dec 02 2018 at 08:23):

@Reid Barton As for doing the day 1 pt 2 in non-meta lean, it was obviously intended to have a solution with unbounded iteration, and it is possible to have such a program never halt on some inputs. With some significant additional work you can actually decide whether an input will halt (by looking at whether the numbers are all distinct mod the period), and so you could get a fully correct non-meta lean solution that way (which is even better than the naive algorithm because it will tell you when the infinite stream has no duplicates).

But if you just want the easy solution, the simplest approach is just to have a depth limiter, and increase it until you get the answer.

Mario Carneiro (Dec 03 2018 at 19:45):

To avoid spamming the chat I won't report daily, but I think I will take up this challenge. Follow along at https://github.com/digama0/advent-of-code (spoiler alert)

Edward Ayers (Dec 04 2018 at 10:45):

On part day 1 part 2, I believe you can show that the search terminates if two elements of your list are equal mod (answer to part 1). So I started coding up a non-meta algorithm but then I realized it would sap away my entire Saturday so I stopped.

Mario Carneiro (Dec 04 2018 at 10:48):

Did you see my solution?

Mario Carneiro (Dec 04 2018 at 10:48):

I did that algorithm

Mario Carneiro (Dec 04 2018 at 10:48):

and it did sap a good chunk of my day ;)

Mario Carneiro (Dec 04 2018 at 10:51):

you can actually do a bit better than producing a proof of well foundedness to run the search... when two values have the same mod the period, you find the least difference of divs, and that's where the search will terminate (so you can do the whole thing without actually running those passes)

Edward Ayers (Dec 04 2018 at 11:03):

Yeah that's how I was going to do it.

Edward Ayers (Dec 04 2018 at 11:10):

@Mario Carneiro thanks for sharing your solutions. There are still lots of language/mathlib features I am neglecting! Eg withtop

Edward Ayers (Dec 04 2018 at 11:52):

Also @Mario Carneiro in the parsers for numbers and letters you can use sat $ char.is_lower and char.is_digit instead of manually checking the char.

Mario Carneiro (Dec 04 2018 at 11:53):

oh, lovely

Mario Carneiro (Dec 04 2018 at 11:54):

I'm hoping that the conventional programming capabilities of lean will be boosted by these attempts

Reid Barton (Dec 02 2020 at 00:07):

Since Lean 4 is supposedly a programming language I thought I'd try it out:
https://github.com/rwbarton/advent-of-lean-4

Reid Barton (Dec 02 2020 at 00:13):

I think it took me about 2 hours to figure out why networking wasn't working in the VM I set up to install Lean 4, 30 minutes to figure out how to read a file, 10 minutes to solve part 1 and 2 minutes to solve part 2 :upside_down:

Yakov Pechersky (Dec 02 2020 at 00:16):

How fast does it run?

Reid Barton (Dec 02 2020 at 00:17):

the ~200^3 algorithm takes about half a second just with lean --run

Reid Barton (Dec 02 2020 at 00:17):

I don't know how to compile it, I should try to figure that out

Marc Huisinga (Dec 02 2020 at 00:25):

https://github.com/leanprover/lean4/tree/master/doc/examples/compiler

Reid Barton (Dec 02 2020 at 00:28):

and I had just figured out the proper incantation

g++ -I ~/lean4/build/release/stage1/include -O -o b b.c -L ~/lean4/build/release/stage1/lib/lean/ -lInit -lleancpp -lLean -lStd -lpthread -lm -lstdc++ -lgmp

Reid Barton (Dec 02 2020 at 00:30):

well it's a lot faster now

Reid Barton (Dec 02 2020 at 00:30):

not sure how accurate these VM timings are but it takes around 0.01 second, will be more interesting for a different program

Marc Huisinga (Dec 02 2020 at 00:32):

slightly prettier WIP docs than using the github interface: https://kha.github.io/lean4/doc

Reid Barton (Dec 02 2020 at 00:35):

I got leanmake working, thanks.

Reid Barton (Dec 02 2020 at 00:37):

There's no jump to definition or autocompletion in the emacs mode right?

Marc Huisinga (Dec 02 2020 at 00:38):

nope. it's as barebones as it gets. the lsp server also doesn't have those features yet.

Reid Barton (Dec 02 2020 at 01:10):

Well, at least that means I can stick to my trusty for now

Marc Huisinga (Dec 02 2020 at 01:15):

i think last we checked the lsp server still worked with emacs' lsp-mode :)

Sebastian Ullrich (Dec 02 2020 at 08:19):

Marc Huisinga said:

slightly prettier WIP docs than using the github interface: https://kha.github.io/lean4/doc

Official, more up-to-date ones at https://leanprover.github.io/lean4/doc/ :)

Alexandre Rademaker (Dec 03 2020 at 12:21):

Hi @Mario Carneiro , any particular reason for using the 2018 problems in your repo?

Mario Carneiro (Dec 03 2020 at 12:21):

Because I did them in 2018?

Mario Carneiro (Dec 03 2020 at 12:23):

Reid's playing the game this year, not me

Alexandre Rademaker (Dec 03 2020 at 12:24):

Hahaha! Sorry ! I though you had started that after @Edward Ayers started this thread!

Reid Barton (Dec 03 2020 at 12:26):

That also happened in 2018

Alexandre Rademaker (Dec 03 2020 at 12:27):

Wow! I am crazy ! I didn’t pay attention to the dates! Ops!

Jason Rute (Dec 06 2020 at 02:14):

@Reid Barton How is this going so far?

Reid Barton (Dec 06 2020 at 02:25):

Pretty well overall. I'd say it's probably already easier than it would be in Lean 3 aside from the editor mode not being finished yet.

Reid Barton (Dec 06 2020 at 02:25):

Basically I pretend I'm writing Haskell except 20% of the time the library function I expect isn't there and I write it myself

Reid Barton (Dec 06 2020 at 02:28):

One problem involved some tricky parsing that was suitable for a parser combinator library which doesn't fully exist, but there's an implementation of a JSON parser which covered enough of what I needed to get the job done

Reid Barton (Dec 06 2020 at 02:28):

which also involved the first time I wrote a destructive update inside a monadic parser

Reid Barton (Dec 06 2020 at 02:28):

I don't really know what it means but I assume the Lean 4 developers figured that out

Marc Huisinga (Dec 06 2020 at 10:45):

Reid Barton said:

which also involved the first time I wrote a destructive update inside a monadic parser

I don't really know what it means but I assume the Lean 4 developers figured that out

if you're holding the only reference to a value, a function that discards that reference just to create some new one can reuse the memory of the value that you're discarding the last reference of.
this commonly comes up in "updates", i.e. you take some structure, change one of its fields and then return the new structure.
imperative programming languages would avoid the allocation through mutation, while functional languages can avoid the allocation through destructive updates.

Reid Barton (Dec 06 2020 at 11:06):

What do mutable variables in a monad desugar to? It can't just be shadowing if you can modify the variable in a loop, right? Some kind of state monad transformer?

Marc Huisinga (Dec 06 2020 at 11:53):

it uses ForInStep (Core.lean#L74, example usage: Basic.lean#L129).
in the above example, f is effectively the body of the for-loop and accumulates a value of type β.
according to Do.lean#L726, β typically denotes the set of variables that are being reassigned.
so i guess it compiles to something similar to a fold that is also capable of more complex control flow?
and then reassignments seem to be just shadowing: Do.lean#L941

Reid Barton (Dec 06 2020 at 12:21):

Thanks, that makes sense.
Now I remember hearing about a mythical Haskell-like language developed by Lennart Augustsson which had things like for loops and while loops...

Reid Barton (Dec 08 2020 at 12:40):

On that note, I guess there are no while loops, even with partial?

Marc Huisinga (Dec 08 2020 at 12:43):

no, there aren't. i think i wanted to ask @Sebastian Ullrich about that at some point :)
core uses let rec usually.

Reid Barton (Dec 08 2020 at 12:50):

It's been fun writing "imperative" pure code... until I wrote seen.set! i true and didn't notice for a while that I meant seen := seen.set! i true :upside_down:

Reid Barton (Dec 08 2020 at 12:51):

Is there some pure trace facility like https://hackage.haskell.org/package/base-4.14.0.0/docs/Debug-Trace.html#v:trace?

Marc Huisinga (Dec 08 2020 at 12:53):

Reid Barton said:

It's been fun writing "imperative" pure code... until I wrote seen.set! i true and didn't notice for a while that I meant seen := seen.set! i true :upside_down:

i think so far every time i've made that mistake the type checker corrected me. did that occur in a function that also happened to have the same return type as seen?

Reid Barton (Dec 08 2020 at 12:54):

It was here https://github.com/rwbarton/advent-of-lean-4/blob/main/8/a.lean#L17

Marc Huisinga (Dec 08 2020 at 12:59):

Reid Barton said:

Is there some pure trace facility like https://hackage.haskell.org/package/base-4.14.0.0/docs/Debug-Trace.html#v:trace?

there's https://github.com/leanprover/lean4/blob/master/src/Init/Util.lean#L15 and https://github.com/leanprover/lean4/blob/master/src/Lean/Util/Trace.lean

Marc Huisinga (Dec 08 2020 at 13:04):

i think the latter may actually not be relevant at all here, sorry!

Reid Barton (Dec 08 2020 at 14:27):

The former looks good though, I'll probably try it out tomorrow.

Jason Rute (Dec 11 2020 at 02:12):

Reid Barton said:

On that note, I guess there are no while loops, even with partial?

It seems pretty easy to make infinite iterators which are functionally the same as while loops but not quite as pretty. (I modified the code for Range.forIn.)

Omri Schwarz (Nov 16 2022 at 20:20):

Hi, all. This year once again I am going to attempt to get through AoC in Lean. I lasted 5 days last year and my kids will probably make this year about as successful, but I'm going through the Functional Programming With Lean online book to be a little better prepared this time around. Anyone else tryin git?

Mario Carneiro (Nov 17 2022 at 20:42):

oh, sweet. For anyone trying it: make sure to take notes on anything missing from Std

Mario Carneiro (Nov 17 2022 at 20:43):

AoC is a great source of reasonable programming tasks that can help boost our coverage

Ryan McCorvie (Nov 26 2022 at 15:23):

I am interested in trying to sharpen my skills with the Advent of Code.

Should we set up a stream to discuss problems?
Should we set up a private leaderboard on the AoC website?

I feel there are some problems which are very natural for Lean, and some which are harder.

Kevin Buzzard (Nov 26 2022 at 15:25):

Why not just start a thread in #lean4 for maximal visibility and if it takes off and you need different threads for different questions you can move to a stream

Adam Topaz (Dec 01 2022 at 15:30):

I probably won't have much more than 30 mins per day to spend on this (which means that I'll probably give up after a few days), but here is my repo for the advent of code 2022 in Lean4, in case anyone else is playing along: https://github.com/adamtopaz/Lean4_AOC_2022

Matej Penciak (Dec 01 2022 at 23:17):

I am also doing the exercises! My repo is here: https://github.com/mpenciak/AdventOfCode

Alex J. Best (Dec 01 2022 at 23:42):

Count me in :wink: https://github.com/alexjbest/aoc

Frédéric Dupuis (Dec 02 2022 at 02:22):

Alright, I'm playing too! https://github.com/dupuisf/Lean4_AoC2022

Ian Riley (Dec 02 2022 at 04:10):

Matej Penciak said:

I am also doing the exercises! My repo is here: https://github.com/mpenciak/AdventOfCode

Where is the best place to learn to write lean code like this? The functional programming manual?

Sebastian Ullrich (Dec 03 2022 at 17:16):

I posted a bit about my updated template on Mastodon: https://types.pl/@kha/109449257306696700
Repo is https://github.com/Kha/aoc-2022

Sebastian Ullrich (Dec 03 2022 at 17:20):

I'm especially interested in perusing the neglected Stream typeclass a bit more like you would in e.g. Rust (/cc @Mario Carneiro, eventually something like this should probably be in std4): https://github.com/Kha/aoc-2022/blob/a15035979a83524ad9908ccf0a2641789a298b78/Aoc/Util.lean#L109-L146

Matei Adriel (Dec 03 2022 at 23:06):

I am new to lean, but I am also trying this out in this repo

Adam Topaz (Dec 03 2022 at 23:51):

Sebastian Ullrich said:

I posted a bit about my updated template on Mastodon: https://types.pl/@kha/109449257306696700
Repo is https://github.com/Kha/aoc-2022

This motivated me to actually (try to) figure out how mastodon works...

Mario Carneiro (Dec 04 2022 at 02:01):

@Sebastian Ullrich Re: Collect, @James Gallicchio has been working a lot on possibilities for iteration typeclasses in std4. It seems like a bit of a quagmire though so I'm trying to avoid the area. ;) I assume that typeclass setup is Rust-inspired?

James Gallicchio (Dec 04 2022 at 04:48):

Ah, yeah, this is definitely related. LeanColls has to do some backflips to avoid external iterators, so if Sebastian finds Stream very ergonomic then that would be a good tradeoff to look at.

Junyan Xu (Dec 04 2022 at 05:12):

https://www.reddit.com/r/adventofcode/comments/zbpq5g/gpt_openai_solutions_should_be_removed_from_the/
https://twitter.com/ostwilkens/status/1598458146187628544

:check: Fully automated solving & submission for #AdventOfCode using #OpenAI text-davinci-003 Can't wait to see how it handles day 2! 🫣 https://twitter.com/ostwilkens/status/1598458146187628544/photo/1

- Carl Öst Wilkens (@ostwilkens)

Junyan Xu (Dec 04 2022 at 07:44):

It's open-sourced: https://github.com/ostwilkens/aoc2022
Can we try the same with Lean? (no need to submit solution quickly if you don't want to)
Day 4 Part 1 champion's methodology:
https://twitter.com/max_sixty/status/1598970226343051264
https://twitter.com/max_sixty/status/1598927902070149120
DeepMind's AlphaCode could probably solve a lot more days; it was about median level on Codeforces when published in February

@ForrestTheWoods @ostwilkens I ran 20 in parallel and submitted the most popular answer — the hit rate is still quite low — both wrong answer and syntax errors Here are some of them: https://twitter.com/max_sixty/status/1598970226343051264/photo/1

- Max (@max_sixty)

@EvgSkvDev @OpenAI @ostwilkens I add some context on it being a puzzle, and do some rudimentary filtering of the text, but otherwise feed it the question without edits https://twitter.com/max_sixty/status/1598927902070149120/photo/1

- Max (@max_sixty)

Sebastian Ullrich (Dec 04 2022 at 08:34):

Another day, another crucial type taken from Rust (spoilers I guess): https://github.com/Kha/aoc-2022/blob/1c99cddba8fabfdccf10adfe37ff4493c9b84805/Aoc/Util.lean#L152-L177

Sebastian Ullrich (Dec 04 2022 at 08:39):

James Gallicchio said:

Ah, yeah, this is definitely related. LeanColls has to do some backflips to avoid external iterators, so if Sebastian finds Stream very ergonomic then that would be a good tradeoff to look at.

I haven't felt any drawbacks yet at least. There may be some questionable typeclass design, but that is independent from the mode of iteration.

Damiano Testa (Dec 08 2022 at 00:43):

Now that the term is almost over, I am starting to have some Lean time: I am also playing!

https://github.com/adomani/Advent_of_Code_2022

Jeremy Salwen (Dec 08 2022 at 01:03):

I am also trying Advent of Code, but I am new to lean. Should be fun :)

Steve Dunham (Dec 08 2022 at 04:51):

Lean was on my short list, but I decided to do Advent of Code in Rust this year. I know neither language. Last Saturday, Sebastian Ulrich's mastodon post inspired me to go back and redo the first three days in Lean. It was fun, so I've been doing it in both languages since then. (The last few days were Lean first.)

Kevin Buzzard (Dec 08 2022 at 08:00):

I'm sure people will be interested in hearing comments about comparison between the two languages!

Sebastian Ullrich (Dec 18 2022 at 12:50):

No Lean involved, but I was just blown away by the visualizations a friend of mine is doing in a Clojure notebook with apparently little effort using Clerk: https://zmb.cm/aoc/2022/2022-18.html. Spoilers, obviously.

Sebastian Ullrich (Dec 18 2022 at 12:50):

Now we just have to get to that level with both widgets and Alectryon :) /cc @Wojciech Nawrocki

Steve Dunham (Dec 18 2022 at 20:01):

That visualization + literate code is nice. I'm not sure I can get to that level of documentation in the time I've got to spend on this, but it's something to aspire to. I'll have to put Clerk on my list of things to check out someday.

I'm still plugging along. The rust is taking a back seat to Lean4, but I'm keeping up in lean. So far Day 16 is the only one I've had to compile - it took about 3.3 minutes to run when compiled (I'm guessing I missed something). I'll share a link to my repository, but with the caveat that I don't really know Lean or Rust: https://github.com/dunhamsteve/aoc2022

Last updated: Dec 20 2023 at 11:08 UTC