Re: [polyml] [ExternalEmail] Compiler (0ad5aa87) raises Option

2020-07-10 Thread Norrish, Michael (Data61, Acton)
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.

Re: [polyml] [ExternalEmail] Compiler (0ad5aa87) raises Option

2020-07-09 Thread Makarius
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

Re: [polyml] [ExternalEmail] Compiler (0ad5aa87) raises Option

2020-07-07 Thread David Matthews
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

Re: [polyml] [ExternalEmail] Compiler (0ad5aa87) raises Option

2020-06-30 Thread Phil Clayton
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

Re: [polyml] [ExternalEmail] Compiler (0ad5aa87) raises Option

2020-06-29 Thread Norrish, Michael (Data61, Acton)
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

Re: [polyml] [ExternalEmail] Compiler (0ad5aa87) raises Option

2020-06-29 Thread Phil Clayton
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

Re: [polyml] [ExternalEmail] Compiler (0ad5aa87) raises Option

2020-06-21 Thread Norrish, Michael (Data61, Acton)
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

Re: [polyml] [ExternalEmail] Compiler (0ad5aa87) raises Option

2020-06-21 Thread Norrish, Michael (Data61, Acton)
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