failed to open file

Stream: new members

[Kenny Lau]

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

[Kenny Lau]

I can't get it to read any file

[Kenny Lau]

it says failed to open file {file name}

[Kenny Lau]

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

[Shing Tak Lam]

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

[Shing Tak Lam]

But there's no output with the #eval

[Kenny Lau]

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

[Shing Tak Lam]

Yeah

[Shing Tak Lam]

You need to escape every backslash

[Kenny Lau]

ok that's the first step

[Kenny Lau]

so it outputs io char_buffer

[Kenny Lau]

which I don't know how to use

[Shing Tak Lam]

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"

[Kenny Lau]

wow thanks!

[Kenny Lau]

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

[Shing Tak Lam]

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?

[Shing Tak Lam]

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

[Kenny Lau]

maybe you can use read/write then?

[Shing Tak Lam]

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...)

[Shing Tak Lam]

I think you can just use k - something though

[Kenny Lau]

that's ok

[Shing Tak Lam]

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.

[Kenny Lau]

I just need 35 numbers / different values

[Mario Carneiro]

one way is to store stuff in the environment

[Kenny Lau]

how do you do that?

[Kenny Lau]

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

[Kenny Lau]

up to 35 times

[Mario Carneiro]

@[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}

[Kenny Lau]

wow, thanks!

[Mario Carneiro]

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

[Kenny Lau]

I guess I don't know attributes

[Mario Carneiro]

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

[Mario Carneiro]

as in, you create increment_1 and increment_2 and so on

[Kenny Lau]

then I would need to parse names?

[Mario Carneiro]

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

[Kenny Lau]

neat

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

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