pirapira / eth-isabelle

A Lem formalization of EVM and some Isabelle/HOL proofs
Other
237 stars 42 forks source link

An ML type error in Apply_Trace.thy with Isabelle2017 #454

Open pirapira opened 7 years ago

pirapira commented 7 years ago

On the branch issabelle2017, when I run

<somewhere where Isabelle2017 was extracted>/Isabelle2017/bin/isabelle build -d . simplewallet

I see


*** Failed to load theory "simplewallet.Apply_Trace_Cmd" (unresolved "simplewallet.Apply_Trace")
*** Failed to load theory "simplewallet.Hoare" (unresolved "simplewallet.Apply_Trace_Cmd")
*** ML error (line 119 of "~/src/eth-isabelle/attic/Apply_Trace.thy"):
*** Type of function does not match type of recursive application.
***    Function:
***       fun
***          proof_body_descend' f get_fact ...
***             =
***             (if ... ... then (... handle ...) else raise ...)
***             handle Option => (... handle ...)
***       : ('a -> bool) ->
***           ('a -> 'b option) ->
***             Inttab.key * ('a * 'c * proof_body future) ->
***               ('a * 'b) option Inttab.table -> ('a * 'b) option Inttab.table
***    Variable: proof_body_descend' :
***       ('a -> bool) ->
***         ('a -> 'b option) ->
***           serial * thm_node ->
***             ('a * 'b) option Inttab.table -> ('a * 'b) option Inttab.table
***    Reason:
***       Can't unify thm_node to 'a * 'b * proof_body future
***          (Incompatible types)
*** At command "ML" (line 18 of "~/src/eth-isabelle/attic/Apply_Trace.thy")
Unfinished session(s): simplewallet
0:02:10 elapsed time, 0:03:35 cpu time, factor 1.65
pirapira commented 7 years ago

@seed told me a workaround: replacing apply_trace with apply.