Loop detection too strict?

[weaversa]

This is pretty strange. At first glance it seems like hitting ctrl-c in the middle of a long running computation make the loop detector get into a bad state.

$ cryptol cryptol-specs/Primitive/Keyless/Hash/SHA1.cry 
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.10.0.99
https://cryptol.net  :? for help

Loading module Cryptol
Loading module Primitive::Keyless::Hash::SHA1
Primitive::Keyless::Hash::SHA1> t3
^CCtrl-C
Primitive::Keyless::Hash::SHA1> t3

<<loop>> (at cryptol-specs/Primitive/Keyless/Hash/SHA1.cry:89:1--89:3, Primitive::Keyless::Hash::SHA1::t3)
Primitive::Keyless::Hash::SHA1> 

[robdockins]

Yes, this is a consequence of the new thunk lifecycle. Basically, the thunk transitions to a state where it has started to be executed, but hasn't yet finished. If you interrupt it, there's no easy way to reset the state back to where it was prior to starting evaluation. If you evaluate it again, it believes the thunk is already under evaluation, and you get the loop error.

I don't know of a great way to handle this situation without incurring a lot of additional bookeeping that is only useful for this exact situation. As a workaround, If you reload the module with :r, it should freshen all the top-level value thunks.

[weaversa]

Perhaps a simple solution is for the <<loop>> error message to mention this issue?

[robdockins]

Yes, that's probably the simplest solution.