Irvin

Is it possible to add a way to compile mlkit with PolyML? @vqns seems to have a working implementation of the ml basis for PolyML https://github.com/vqns/polymlb

Try to store only delta's in translator Part 1

1

This is quite a bad way but still better than the old way Progress list. 1. unpack_types --done 2. unpack_v_thms 3. unpack_cons_names 4. unpack_type_mods

Better simplification of preconditions for eq_lemmas

1

Looking at the result of eq_lemmas after calling ``val _ = translation_extends "decProg";`` in the front of to_flatProgTheory it seems some theorems stored have unnecessary T in the implication ```...

Get compiler/proofs to under 50 minutes on CakeML regression servers

1

follow up of #1243. We can always be faster :)

https://github.com/CakeML/cakeml/blob/6ddaf6f8d86d8d5f57f0bcfc8fdd78f855e3daae/compiler/backend/proofs/flat_to_closProofScript.sml#L72-L76 OPTREL should be used instead.

Implement parser that supports unsupported features

2

When writing CakeML code/porting code from other ml implementations one would accidentally use features that CakeML currently doesn't support. This issue is not proposing to implement these features but make...

Refactor to remove Eq_result type

1

It's unnecessary and doesn't make code much clearer. It can be replaced with bool option. The advantage of using option is that do_eq_list can be written using OPT_MMAP or maybe...

Having it as a builtin op would be nice but adding a function defined as `fun abs n = if n < 0 then ~ n else n` would be...

This issue is about implementing what Haskell calls arity analysis. https://www.joachim-breitner.de/publications/CallArity-ICFP2015-preprint.pdf. I think this will involve a pass that just does eta expansion of functions before getting a more general...

This will probably be done by setting up the extensible pretty printer for exceptions and then exporting it.