[isabelle] Error Building HOL-Word



Hi Isabelle-Users,

I am trying to compile some files from the eth-isabelle
<https://github.com/pirapira/eth-isabelle> project using the command-line
version of Isabelle (e.g. isabelle process -T TheoryName). It seems like
the error is due to a dependency on the HOL-Word library.

In fact, I notice that the HOL-Word library fails to build. When I run
isabelle build HOL-Word, I get a failure with the following error (at the
end):

### theory "HOL-Word.WordBitwise"
### 0.591s elapsed time, 2.297s cpu time, 0.234s GC time
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "apply" (line 284 of
"~~/src/HOL/Word/Bit_Representation.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 12 of "~~/src/HOL/Word/Misc_Numeric.thy")
Unfinished session(s): HOL-Word
0:00:37 elapsed time, 0:01:11 cpu time, factor 1.91

I assume this isn't expected behavior for trying to build HOL-Word (but let
me know if I'm wrong about that).

Strangely, this doesn't appear to be a problem when I open the files that
require this dependency in the JEdit interface to Isabelle: the file
processes successfully without any errors. Do you have any ideas why this
might be failing and what I can do to get it to build?

Best,
Mario



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.