Zulip Chat Archive

Stream: lean4

Topic: initializing data from IO

Arthur Paulino (Dec 08 2022 at 18:05):

Suppose I have a foo : IO Nat that reads a natural number from a text file and I want to load it into a constant const : Nat. How can I do this?

From the following comment, I got the impression that this it doable via initialize. Did I understand it correctly?

Mario Carneiro said:

initialize foo : HashMap A B <- (bla : IO (HashMap A B))

Arthur Paulino (Dec 08 2022 at 18:12):

This works:

def foo : IO Nat := sorry
initialize const : Nat ← foo

But this doesn't

def readCache : IO $ Std.RBMap (Nat × Nat) (MultilinearPolynomial $ Zmod n) compare := do
  match Json.parse (← IO.FS.readFile ⟨"YatimaStdLib/MLE/cache.json"⟩) with
  | .error e => panic! e
  | .ok cachedJson => match jsonToCachedMLPs cachedJson with
    | .error e => panic! e
    | .ok cache => pure cache

initialize multilinearLagrangePolynomialCache :
  (Std.RBMap (Nat × Nat) (MultilinearPolynomial $ Zmod n) compare) ← readCache
-- initialization function 'MLE.initFn._@.YatimaStdLib.MLE.MultilinearExtension._hyg.1040'
-- must have type of the form `IO <type>`

Arthur Paulino (Dec 08 2022 at 18:16):

Hmm, apparently it's the parameter n :thinking:

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

Yeah, it's not a datum if it has a parameter

Arthur Paulino (Dec 08 2022 at 18:51):

Right, I have another idea in mind that will surely work. Thanks!

Arthur Paulino (Dec 29 2022 at 14:23):

Is there some known problem with initializing some data types? I haven't been able to make it work for UInt64 nor Bool.
This is the error fro UInt64:

error: > /home/arthur/.elan/toolchains/leanprover--lean4---nightly-2022-12-16/bin/leanc -c -o ./build/ir/Cache/IO.o ./build/ir/Cache/IO.c -O3 -DNDEBUG
error: stderr:
./build/ir/Cache/IO.c:9280:21: error: incompatible pointer to integer conversion assigning to 'uint64_t' (aka 'unsigned long') from 'b_lean_obj_res' (aka 'lean_object *') [-Wint-conversion]
l_Cache_IO_rootHash = lean_io_result_get_value(res);
                    ^ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1 error generated.
error: external command `/home/arthur/.elan/toolchains/leanprover--lean4---nightly-2022-12-16/bin/leanc` exited with code 1

The error for Bool is similar. It works on the kernel, but not on compiled code

Arthur Paulino (Dec 29 2022 at 14:28):

Since it works for Nat, I'm doing this as a workaround for now:

initialize rootHashFix : Nat ← getRootHash

def rootHash : UInt64 :=
  .ofNat rootHashFix

Henrik Böving (Dec 29 2022 at 15:52):

(deleted)

Henrik Böving (Dec 29 2022 at 15:54):

Yeah that seems to be missing support for unboxed types. THe compiler would have to insert a lean_unbox in this situation.

Henrik Böving (Dec 29 2022 at 16:00):

we should definitely fix this in the new compiler and maybe also in the old one if someone is up for that, you can open an issue for it on the compiler repo I think @Arthur Paulino

Arthur Paulino (Dec 29 2022 at 16:07):

There is a compiler repo? Or is it https://github.com/leanprover/lean4 itself?

Henrik Böving (Dec 29 2022 at 16:11):

The second yes.

Arthur Paulino (Dec 29 2022 at 16:24):

https://github.com/leanprover/lean4/issues/1998 :+1:

Trebor Huang (Dec 30 2022 at 01:16):

Does haskell have a similar function, by the way?

Mario Carneiro (Dec 30 2022 at 01:35):

I found Data.FileEmbed, which seems to suggest that Template Haskell is the usual way to do compile-time IO

Last updated: Dec 20 2023 at 11:08 UTC