[CakeML] Basis library

[Scott Owens]

Hi Lars,

To get output you need one extra step, which is to write a CakeML program directly that will call the HOL4 extracted function and print the answer. You can use our implementation of CF (characteristic formula) program logic to prove things about what the program prints. cakeml/characteristic/examples/echoProgScript.sml has an example of doing this.

Scott

> On 2017/07/20, at 14:38, Lars Hupel <hupel at in.tum.de> wrote:
> 
> Hi Ramana,
> 
>> I put the result of running the following code at
>> https://cakeml.org/basis-names.txt for now. (But don't expect that link to
>> be kept up to date, or even alive.)
> 
> that's perfect! No need to keep it alive. I'm currently experimenting
> with the bootstrapped snapshot you sent me in April (based on 32b749c3).
> 
> I'm mostly interested in string manipulation though, because in my work,
> I need to print the result of my generated program. Otherwise, my
> program would just "generate heat" and the user could not observe the
> result. How do you deal with this in the HOL4 extraction? Can the user
> say "generate me a program that computes `fib 5` and prints the result"?
> 
> Cheers
> Lars
> 
> _______________________________________________
> Users mailing list
> Users at cakeml.org
> https://lists.cakeml.org/listinfo/users