Irvin
Irvin
Allowing candle to use this would be explicit goal.
It would a proof of equivalence between 1. run candle and "build" the base library. Export the heap state. Create a new instance of cakeml pass it the heap state...
Related issue #880
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...
See https://github.com/llvm/llvm-project/blob/main/llvm/lib/Transforms/InstCombine/InstCombineMulDivRem.cpp for the llvm's implementation
Isn't that issue about adding shifts for every pass from Source. wordlang already has shift instructions.
https://github.com/HOL-Theorem-Prover/HOL/blob/78876ba822649556a9b0bc45047a0935d007995c/INSTALL#L171 @mn20 mentioned to me that this email address has been closed
See comment by @myreen https://hol.zulipchat.com/#narrow/channel/518311-CakeML-issue-review/topic/Improve.20implementation.20of.20Vector.2Etabulate.20.23411/near/531273893 > > This should be open. > I'm still of the opinion that option 2 is the right way to go, but we could have...
I would not associate an S3 bucket with cheap. Using a S3 compatible api maybe but not aws s3.
Bonus points implement a way to get a unique name in linear time. This can be done using the fact that `a