search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
630 stars 142 forks source link

HOL/examples/formal-languages build failure #417

Closed SOwens closed 7 years ago

SOwens commented 7 years ago

I've just updated to PolyML 5.7, and charsetTheory fails to build. (Different type constructors) Found near if ~>> (w, ... ...) = 1 then orb (w, IntInf.<< (...)) else w /Users/sao/HOL/examples/formal-languages/regular/WordOps.sml:28: error: Type error in function application. Function: Word.fromInt : Int.int -> Word.word Argument: width : int Reason: Can't unify Int.int (In Basis) with int (In Basis) (Different type constructors) Found near if ~>> (w, ... ...) = 1 then orb (w, IntInf.<< (...)) else w Static Errors

konrad-slind commented 7 years ago

Probably the regexp library hasn't been upgraded to the downgrade from the paradise of IntInf = Int. Anthony had pinged me about this awhile ago, but I hadn't gotten to it. He may have fixes already, if my memory is right.

Konrad.

On Tue, May 9, 2017 at 11:50 AM, Scott Owens notifications@github.com wrote:

I've just updated to PolyML 5.7, and charsetTheory fails to build. (Different type constructors) Found near if ~>> (w, ... ...) = 1 then orb (w, IntInf.<< (...)) else w /Users/sao/HOL/examples/formal-languages/regular/WordOps.sml:28: error: Type error in function application. Function: Word.fromInt : Int.int -> Word.word Argument: width : int Reason: Can't unify Int.int (In Basis) with int (In Basis) (Different type constructors) Found near if ~>> (w, ... ...) = 1 then orb (w, IntInf.<< (...)) else w Static Errors

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/417, or mute the thread https://github.com/notifications/unsubscribe-auth/ABDgD-a8kMZgj5oz_-nsmEE3HTwpEyJbks5r4JlWgaJpZM4NVlz1 .

acjf3 commented 7 years ago

I do have a fix. However, it may be best to put it on a fresh branch? The original library authors will need to test it and check that it works as expected.

acjf3 commented 7 years ago

You can try the commit c9bc095.

konrad-slind commented 7 years ago

Thanks Anthony! --Konrad.

On Wed, May 10, 2017 at 3:46 AM, acjf3 notifications@github.com wrote:

You can try the commit c9bc095 https://github.com/HOL-Theorem-Prover/HOL/commit/c9bc09512e72ac7fc0f6708d0f9af3060bb9a735 .

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/417#issuecomment-300416783, or mute the thread https://github.com/notifications/unsubscribe-auth/ABDgD9sNnPp_LzFdVUEL0aRbjtqr0LZ9ks5r4XlsgaJpZM4NVlz1 .

SOwens commented 7 years ago

It's worth noting that CakeML depends on this example building, so it's worth getting the fix onto master soon.

xrchz commented 7 years ago

I made a pull request for it (#420). I think the original authors are @konrad-slind and/or @mn200 - and clearly Konrad is OK with this fix?

konrad-slind commented 7 years ago

Bit busy at the moment (paper deadlines). I promise to have a look tomorrow. Anthony made the fixes BTW.

Konrad.

On Mon, May 15, 2017 at 11:21 PM, Ramana Kumar notifications@github.com wrote:

I made a pull request for it (#420 https://github.com/HOL-Theorem-Prover/HOL/pull/420). I think the original authors are @konrad-slind https://github.com/konrad-slind and/or @mn200 https://github.com/mn200 - and clearly Konrad is OK with this fix?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/417#issuecomment-301671556, or mute the thread https://github.com/notifications/unsubscribe-auth/ABDgD2z3nOeeZ5PouuBgJALe5jb-3Pmaks5r6SQ2gaJpZM4NVlz1 .

xrchz commented 7 years ago

420 was merged, so closing this