[CakeML-dev] Holmake bug

Michael.Norrish at data61.csiro.au Michael.Norrish at data61.csiro.au
Wed Dec 7 10:45:19 UTC 2016

I saw your fixes thanks. 

Nonetheless, I am still getting an error caused by the fact that holSyntaxLibTheory doesn’t spot that it depends on lprefix_lub.


On 7/12/16, 17:03, "Ramana Kumar" <Ramana.Kumar at cl.cam.ac.uk> wrote:

    I have often got lprefix_lub errors in various places, but I think
    they all went away when following the policy of listing all INCLUDEs
    explicitly (i.e., not relying on ones built into the heap).
    (By the way, fixes to readerTheory are merged into master already (in
    case you were trying to fix it..))
    On 7 December 2016 at 16:52,  <Michael.Norrish at data61.csiro.au> wrote:
    > Do others get a lprefix_lub error when attempting to build readerTheory in candle/standard/opentheory?
    > I think this is a bug in Holmake, but I’m surprised it hasn’t bothered anyone else.
    > There’s a relatively simple workaround that I can commit, but I also want to figure out why Holmake is not doing the right thing when it does its dependency analysis of holSyntaxLibTheory.sml.
    > Michael
    > _______________________________________________
    > Developers mailing list
    > Developers at cakeml.org
    > https://lists.cakeml.org/listinfo/developers

More information about the Developers mailing list