Load a string as a def so native_decide sees it, not oleans

Stream: lean4

[Geoffrey Irving]

I have some code of the following form:

def certificate : String := <metaprogram that loads an enormous string from a file during>

def P : Prop := ...

def check : String -> Bool := ..

theorem check_implies_p (s : String) : check s = True -> P := ...

theorem p : P := by
  apply check_implies_p certificate
  native_decide

My problem is that certificate is over 8 GB. If I copy it or save it to an .olean file, all is lost and I get out-of-memory crashes. What's the best way to proceed in this situation? I'm aware that native_decide is sad, of course, but it's hard to avoid it in the situation (generating the certificate is done in Rust or CUDA and takes a long time).

[Geoffrey Irving]

Aha, possibly module will do this.

[Eric Wieser]

You could perhaps use @[extern] and implement the file reading as a C function

[Eric Wieser]

docs#unsafeIO might also work for you

[Henrik Böving]

Eric Wieser said:

You could perhaps use @[extern] and implement the file reading as a C function

That usually allows for pretty easy proofs of false though. I had contemplated this for bv_decide as well

[Eric Wieser]

I guess it's equivalent to the unsafeIO approach?

[Henrik Böving]

More or less yes

[Henrik Böving]

It feels to me like there should be some sort of paging technique that can be abused here tho