compiler bug aborts build of istari #337

Version

110.99.7 (Latest)

Operating System

• Any
• Linux
• macOS
• Windows
• Other Unix

OS Version

Sequoia 15.1.1

Processor

• Any
• Arm (using Rosetta)
• PowerPC
• Sparc
• x86 (32-bit)
• x86-64 (64-bit)
• Other

System Component

Core system

Severity

Major

Description

Cannot build Crary's Istari prover (istarilogic.org) because of compiler bug below.

Transcript

[compiling ../prover/(prover.cm):../ipp/basis/(basis.cm):basis.sml]
Error: Compiler bug: IntInfCnv: toInf: incorrect number of arguments
val it = false : bool
export.sml:22.32-22.47 Error: unbound structure: Handler in path Handler.handler
make[1]: *** [batch-nolib] Error 1
make: *** [smlnj] Error 2

Expected Behavior

It should compile :).

Steps to Reproduce

Just download istari from istarilogic.org and build on a Mac (notebook or desktop failed for me). It will fall over as indicated above. Seems to be a bug with bignum's.

Additional Information

No response

Email address

rwh@cs.cmu.edu