Thanks for your work on this! The HOL4 code that was causing the Option
exception previously now compiles fine.
Michael
On 7/7/20, 16:43, "polyml on behalf of David Matthews"
wrote:
Thanks for producing this example. I've investigated it and the current
master ( fb10196 ) includes a fix.
On 07/07/2020 08:41, David Matthews wrote:
> Thanks for producing this example. I've investigated it and the current
> master ( fb10196 ) includes a fix.
>
> The current master should have proper fixes for both the bugs.
> Makarius: Could you check that you don't get the segfault in the
Thanks for producing this example. I've investigated it and the current
master ( fb10196 ) includes a fix.
This turned out to be more complicated than expected. Earlier in the
year Makarius reported a segfault in some generated code and produced a
cut down example. Reverting a change
I managed to produce a smallish example fairly quickly as the code
causing it didn't have many dependencies. I have raised
https://github.com/polyml/polyml/issues/136
Phil
On 30/06/20 00:14, Norrish, Michael (Data61, Acton) wrote:
No, I'm afraid not. I will try to find some time to find a
No, I'm afraid not. I will try to find some time to find a MWE this week.
Michael
On 30/6/20, 02:54, "polyml on behalf of Phil Clayton"
wrote:
I, too, am seeing this error message with the latest master (ef44a8b).
Michael - did you make any progress with this issue?
Phil
On 22/06/20
I, too, am seeing this error message with the latest master (ef44a8b).
Michael - did you make any progress with this issue?
Phil
On 22/06/20 02:18, Norrish, Michael (Data61, Acton) wrote:
Sorry to spam (will take this elsewhere after this).
The "workaround" below doesn't help in the wider
Sorry to spam (will take this elsewhere after this).
The "workaround" below doesn't help in the wider context. If I select all of
the code without the enclosing
structure helperLib :> helperLib = struct ... end
it compiles without error, but if I have the enclosure, I again get the same
I get a workaround by lifting the definition of find_term_and_apply out to the
top-level.
Michael
On 22/6/20, 10:54, "polyml on behalf of Norrish, Michael (Data61, Acton)"
wrote:
I don't expect this in isolation will help, but the following HOL function
causes the compiler to emit a
