Zulip Chat Archive

Stream: new members

Topic: failed to open file


view this post on Zulip Kenny Lau (May 16 2020 at 07:12):

import system.io
#eval io.fs.read_file "{any file}"

view this post on Zulip Kenny Lau (May 16 2020 at 07:12):

I can't get it to read any file

view this post on Zulip Kenny Lau (May 16 2020 at 07:12):

it says failed to open file {file name}

view this post on Zulip Kenny Lau (May 16 2020 at 07:13):

do I need to give the full address? is it in /c/ convention or C:\ convention?

view this post on Zulip Shing Tak Lam (May 16 2020 at 07:47):

I got the error to go away by providing the full path, with the C:\ convention

view this post on Zulip Shing Tak Lam (May 16 2020 at 07:48):

But there's no output with the #eval

view this post on Zulip Kenny Lau (May 16 2020 at 07:49):

you actually used the C:\\ convention didn't you

view this post on Zulip Shing Tak Lam (May 16 2020 at 07:49):

Yeah

view this post on Zulip Shing Tak Lam (May 16 2020 at 07:49):

You need to escape every backslash

view this post on Zulip Kenny Lau (May 16 2020 at 07:50):

ok that's the first step

view this post on Zulip Kenny Lau (May 16 2020 at 07:50):

so it outputs io char_buffer

view this post on Zulip Kenny Lau (May 16 2020 at 07:50):

which I don't know how to use

view this post on Zulip Shing Tak Lam (May 16 2020 at 07:58):

This works (outputs a list of characters), but that's easy to convert to other data types if necessary.

import system.io

def test (file_name : string) : io unit :=
do
  s <- io.fs.read_file file_name,
  io.print (buffer.to_list s)

#eval test "C:\\Users\\Shing\\Desktop\\Test\\leanpkg.toml"

view this post on Zulip Kenny Lau (May 16 2020 at 07:58):

wow thanks!

view this post on Zulip Kenny Lau (May 16 2020 at 08:00):

@Shing Tak Lam do you think you can do the next step then?

view this post on Zulip Shing Tak Lam (May 16 2020 at 08:08):

I don't know. I tried get_line but that just reads the first line of the file every time... Is there a function that keeps track of where it's read so far?

view this post on Zulip Shing Tak Lam (May 16 2020 at 08:08):

and io.fs.read seems to start at the beginning every time.

view this post on Zulip Kenny Lau (May 16 2020 at 08:09):

maybe you can use read/write then?

view this post on Zulip Shing Tak Lam (May 16 2020 at 08:15):

import system.io

def test (file_name : string) : io unit :=
do
  h <- io.mk_file_handle file_name io.mode.read,
  s <- io.fs.get_line h,
  let k := char.to_nat (list.head (buffer.to_list s)),
  h' <- io.mk_file_handle file_name io.mode.write,
  io.fs.write h' (list.to_buffer [(char.of_nat (k + 1)), '\n']),
  io.print k

#eval test "C:\\Users\\Shing\\Desktop\\Test\\test.txt"
#eval test "C:\\Users\\Shing\\Desktop\\Test\\test.txt"
#eval test "C:\\Users\\Shing\\Desktop\\Test\\test.txt"

This prints out consecutive numbers (but it doesn't start at 0...)

view this post on Zulip Shing Tak Lam (May 16 2020 at 08:16):

I think you can just use k - something though

view this post on Zulip Kenny Lau (May 16 2020 at 08:17):

that's ok

view this post on Zulip Shing Tak Lam (May 16 2020 at 08:19):

Also this isn't storing the number in the file, it's just storing the ASCII (or Unicode idk) of that value, so I don't think the new lines are necessary.

view this post on Zulip Kenny Lau (May 16 2020 at 08:19):

I just need 35 numbers / different values

view this post on Zulip Mario Carneiro (May 16 2020 at 08:20):

one way is to store stuff in the environment

view this post on Zulip Kenny Lau (May 16 2020 at 08:22):

how do you do that?

view this post on Zulip Kenny Lau (May 16 2020 at 08:28):

ideally I would want

def first_time : nat := by increment
def second_time : nat := by increment
def third_time : nat := by increment

to give different results

view this post on Zulip Kenny Lau (May 16 2020 at 08:28):

up to 35 times

view this post on Zulip Mario Carneiro (May 16 2020 at 08:31):

@[user_attribute]
meta def incr_attr : user_attribute unit  :=
{ name   := `incrementer,
  descr  := "incrementer",
  parser := pure 0 }

open tactic
meta def increment : tactic unit :=
do n  incr_attr.get_param `increment <|> pure 0,
  tactic.trace n,
  incr_attr.set `increment (n+1) tt

run_cmd increment -- 0
run_cmd increment -- 1
run_cmd increment -- 2
example   : true := by {increment, /- 3 -/ increment, /- 4 -/ triv}
theorem T : true := by {increment, /- 3 -/ increment, /- 4 -/ triv}
def     U : true := by {increment, /- 3 -/ increment, /- 4 -/ triv}
def     V : true := by {increment, /- 5 -/ increment, /- 6 -/ triv}

view this post on Zulip Kenny Lau (May 16 2020 at 08:32):

wow, thanks!

view this post on Zulip Mario Carneiro (May 16 2020 at 08:33):

If you #print increment you will see the magic: increment sets an attribute on itself when called

view this post on Zulip Kenny Lau (May 16 2020 at 08:34):

I guess I don't know attributes

view this post on Zulip Mario Carneiro (May 16 2020 at 08:34):

You don't have to use attributes - you could equally well use new definitions

view this post on Zulip Mario Carneiro (May 16 2020 at 08:34):

as in, you create increment_1 and increment_2 and so on

view this post on Zulip Kenny Lau (May 16 2020 at 08:35):

then I would need to parse names?

view this post on Zulip Mario Carneiro (May 16 2020 at 08:35):

and each call to the tactic creates a new definition, and then you count how many definitions have been made so far

view this post on Zulip Kenny Lau (May 16 2020 at 08:35):

neat

view this post on Zulip Mario Carneiro (May 16 2020 at 08:35):

Here you have to run exprs, which is at least as expensive as parsing names

view this post on Zulip Kenny Lau (May 16 2020 at 08:36):

is there any way to make it an actual definition though? like not just calling tactic.trace

view this post on Zulip Mario Carneiro (May 16 2020 at 08:36):

Note that the changes don't stick when the call is inside an example or theorem, because the environment is rolled back after elaboration


Last updated: May 17 2021 at 21:12 UTC