Yong Kiam
Yong Kiam
Isabelle's datatype package introduces a bunch of helpful constants on datatype definitions, see 2.1.5 Auxiliary Constants http://isabelle.in.tum.de/dist/Isabelle2020/doc/datatypes.pdf (thanks to @IlmariReissumies for the link) These seem like they could be nice...
Following Ramana's recent email to the users' list, I gave Holyhammer a try. Here're two features that, I think, would make interaction easier (in Vim or Emacs): 1) Shortcut to...
This issue is about adding support for the bitmap and code buffers to all of the exporters (except x64, which already has them).
This should involve modify unverified/reg_alloc/reg_alloc.sml (and files that use it) to print the relevant names instead of the function index. Suggested by @myreen
This issue is about adding instructions, e.g., to developers/, for 1. Profiling a CakeML program (using @sorear 's symbol additions) 2. Extracting intermediate dataLang code from the compiler This was...
This issue is about setting up an alternative pathway to call into CakeML-generated code from C/C++. Right now, the default exporter only allows running CakeML code as the "main" function....
This issue is about speeding up prototyping of code that is (to be) verified using the translator and/or CF. Currently, the process I used is roughly: 1. write HOL definitions...
This revives issue #260 The goal is to instead use Runtime.exit and prove the required CF and whole prog spec for the compiler instead of relying on the current approach....
The default list sort has quadratic behavior on sorted (or nearly sorted) lists because it picks the pivot from the head of the list. This issue is about potentially replacing:...
Also create a howto.md for it (As discussed with @myreen )