Oskar Abrahamsson
Oskar Abrahamsson
I don't know if it's possible for HOL to deduce the true path of a theory's source file from the name of the theory, but if it isn't, then perhaps...
I came across this when I found that some of our code apparently relied on a one-to-one correspondence between `Lang.cf` and the names of directories generated by BNFC: clearly not...
> One could address a slightly broader question: should the translator mangle names at all and if so how? I agree that it should be an option whether or not...
@agomezl where is the work done so far, is it on a branch somewhere?
The most annoying issue is that command-line arguments are dealt with in two places: * [In the main function in compiler64ProgScript.sml](https://github.com/CakeML/cakeml/blob/master/compiler/bootstrap/translation/compiler64ProgScript.sml), and * [In the pure compiler function in compilerScript.sml](https://github.com/CakeML/cakeml/blob/master/compiler/compilerScript.sml)....
* To get an arm64 compiler binary out of the bootstrap runs, you also need to add your target to this file: https://github.com/CakeML/cakeml/blob/master/developers/build-sequence. * The 32-bit arm8 target seems unnecessary:...
This code will run very often. Maybe it would be worth the effort to go with (2)?
> Have you considered recording the OpenTheory proofs by adding additional assumptions to the recorded theory corresponding to facts produced by the compute rule? I think OpenTheory kinda supports oracles...
Bootstrapping many targets has recently become much faster. I think this issue should be closed by #1022.
Closed by #1022.