Remove Q.prove in ml_monad_translator_interfaceLib

Open ordinarymath opened this issue 9 months ago • 2 comments

As in title. Right now loading that Library is extremely slow.

Apr 04 '25 01:04 ordinarymath

Hello! I would like to work on this issue, can you give me some instructions?

Apr 06 '25 01:04 haveheartt

Hi do you have experience with HOL. This issue is about removing top level uses of Q.prove in a https://github.com/CakeML/cakeml/blob/master/translator/monadic/ml_monad_translator_interfaceLib.sml and moving them to https://github.com/CakeML/cakeml/blob/master/translator/monadic/ml_monad_translatorScript.sml.

Here's an example of a top_level Q.prove https://github.com/CakeML/cakeml/blob/43b8014f368073c1b7bf32d38bae36ea9e04ad63/translator/monadic/ml_monad_translator_interfaceLib.sml#L533C1-L538C1

This is in a function and not a top level Q.prove https://github.com/CakeML/cakeml/blob/43b8014f368073c1b7bf32d38bae36ea9e04ad63/translator/monadic/ml_monad_translator_interfaceLib.sml#L365C1-L368C6

Apr 06 '25 04:04 ordinarymath