Zulip Chat Archive

Stream: new members

Topic: File io in Lean 3

Ocschwar (Dec 01 2021 at 23:57):

Hello, all. I started on Advent of Code, so now's the time to get stuck on simple file IO. I'm plagiarizing the Advent of Lean 3 stuff, but am a little bit stuck. I'm trying to get this function to return (list \alpha) ):

def go {α} (file : string) (p : parser α) (m : α → option string) : io unit :=
do s ← io.fs.read_file file,
  sum.inr a ← return $ run p s,
  some str ← return $ m a,
  trace str (return ())

Kevin Buzzard (Dec 01 2021 at 23:58):

You're not tempted to use Lean 4?

Ocschwar (Dec 01 2021 at 23:58):

What do I do to get this to return the right value?

Ocschwar (Dec 01 2021 at 23:59):

I am tempted, but I've invested the time I have between work and kids to learn Lean 3, so sunk cost fallacy has a strong hold on me.

Ocschwar (Dec 02 2021 at 00:00):

BTW, I'm going through your Xena Project videos right now as well, and after umpteen attempts at mastering formal methods tools, this is actually taking.

Kevin Buzzard (Dec 02 2021 at 00:01):

I don't have a clue about tactics or coding, so I'm sorry I can't help you.

Kevin Buzzard (Dec 02 2021 at 00:01):

One thing I would say is that you haven't posted a #mwe -- if I paste the code you posted into a Lean file I just get a ton of errors. It's generally easier to help people if they post #mwe s.

Ocschwar (Dec 02 2021 at 00:05):

I'll do that as soon as. have something that's working.

Adam Topaz (Dec 02 2021 at 00:07):

If you want the return value to be list X, then your go function should probably have type io (list X).

Kyle Miller (Dec 02 2021 at 00:09):

here's a #mwe I think:

import tactic

open parser

def go {α} (file : string) (p : parser α) (m : α → option string) : io unit :=
do s ← io.fs.read_file file,
  sum.inr a ← return $ run p s,
  some str ← return $ m a,
  trace str (return ())

Adam Topaz (Dec 02 2021 at 00:10):

FWIW, today was the first time I tried coding in lean4, and I got the first advent of code puzzle in about 15 mins. Lean4 is REALLY nice.

Kyle Miller (Dec 02 2021 at 00:13):

Ocschwar said:

What do I do to get this to return the right value?

What's the list \alpha that you want supposed to represent? Are you wanting to run the parser p on each line of the file or something?

Ocschwar (Dec 02 2021 at 00:17):

Yes. I'm using this https://github.com/digama0/advent-of-code/blob/lean-3.4.1/day1.lean and I need to take \n-separated integers to return (list \N)

Kyle Miller (Dec 02 2021 at 00:25):

@Ocschwar Completely untested:

import tactic

open parser

/- cribbed from io.fs.read_to_end and modified -/
def parse_lines {α} (h : io.handle) (p : parser α) : io (list α) :=
io.iterate [] (λ parsed,
  do done ← io.fs.is_eof h,
     if done
     then return none
     else do s ← io.fs.get_line h,
             sum.inr a ← return $ run p s,
             return $ some $ parsed ++ [a])

def parse_file {α} (file : string) (p : parser α) : io (list α) :=
do h ← io.mk_file_handle file io.mode.read ff,
   parse_lines h p

Ocschwar (Dec 02 2021 at 00:29):

Wow, thank you ! I'll post the link to my GitHub repo once it's created and populated.
(My motivation is that I QA R code for a living, and so I daydream about languages that let you write R-ish code, then prove some sanity checks about the mathematical properties of the outputs that then become compile time checks on any changes you make. Lean appears to come closest to enabling that. )

Ocschwar (Dec 02 2021 at 00:31):

Which means my formal methods background and higher math background is very superficial, and I have no direct financial interest in where tools like TLA+ and Alloy have been applied so far (security properties, safe concurrency, etc). So Lean also is best for pushing up the learning curve.

Last updated: Dec 20 2023 at 11:08 UTC