Flush stdout after outputting debug message

[someplaceguy]

TextIO.output() doesn't flush stdout, but print() does. Flushing is necessary to make sure the messages are printed in a timely fashion, which is important when debugging timing/performance issues.

The performance hit of the extra flushing should be negligible, as even when these debug messages are enabled, they are only printed a few dozen times or so.

[someplaceguy]

#13 2381.8 FactTheory examples/dev (9s)FAIL<Signal B>

This segmentation fault in the docker test seems quite concerning, although I'd be surprised if it was related to this PR...

[mn200]

Thanks for this!

The issue with examples/dev is a known problem with our regression/CI infrastructure that we haven't yet been able to figure out. I have other regression tests running that will pick things up if there really are problems (which, as you say, are utterly unlikely with this commit).

[someplaceguy]

The issue with examples/dev is a known problem with our regression/CI infrastructure that we haven't yet been able to figure out.

It's really hard for me to say for sure as I haven't been able to reproduce that problem, but I found polyml/polyml#189, which might be what is causing that segfault.

If so, I think I figured out how to reproduce it, as I mentioned in my comment on that issue: polyml/polyml#189 (comment)

[someplaceguy]

It's really hard for me to say for sure as I haven't been able to reproduce that problem, but I found polyml/polyml#189, which might be what is causing that segfault.

I'm now pretty sure that this is exactly the bug that is causing the CI failures.

In a previous comment I quoted the failing message:

#13 2381.8 FactTheory examples/dev (9s)FAIL<Signal B>

The examples/dev directory contains exactly the line of code that I identified as causing the Poly/ML segfault (although, it only happens on some locales as I mentioned in that bug):

$ grep -F Date.fmt examples/dev -r
examples/dev/vsynth.sml:fun date() = Date.fmt "%c" (Date.fromTimeLocal (Time.now ()));

[mn200]

Aha; many thanks for all of the detective work that has led to this point! I will provide a stub implementation of date in that example as a workaround until the PolyML/glibc issue is resolved.

[someplaceguy]

Aha; many thanks for all of the detective work that has led to this point! I will provide a stub implementation of date in that example as a workaround until the PolyML/glibc issue is resolved.

Sure, no problem!

However, note that there are also other examples that will likely run into the same issue. Specifically, these ones:

$ grep -F 'Date.fmt "%c"' . -r
./examples/dev/vsynth.sml:fun date() = Date.fmt "%c" (Date.fromTimeLocal (Time.now ()));
./examples/acl2/ml/sexp.sml:fun date() = Date.fmt "%c" (Date.fromTimeLocal (Time.now ()));
./examples/acl2/examples/M1/sexp.sml:fun date() = Date.fmt "%c" (Date.fromTimeLocal (Time.now ()));
./examples/acl2/examples/acl2-hol-ltl-paper-example/sexp.sml:fun date() = Date.fmt "%c" (Date.fromTimeLocal (Time.now ()));

As an alternative to stubbing Date.fmt, you could instead make sure that the environment variable LC_TIME is set to C or POSIX (e.g. in the corresponding Holmakefiles, perhaps?) before the offending code runs, which would also avoid the crash. That said, I'm not sure which workaround is cleaner, as my knowledge about HOL4 is very limited.

[binghe]

@someplaceguy thank you so much for finding out the root cause of this annoy Poly/ML crashing. So it doesn't crash on macOS (which I use daily) because the bug is in glibc on Linux (at least). It's definitely possible to force the locale to C in docker CI builds but this is no more necessary since Michael has disabled the time printing in examples/dev.

[mn200]

The acl2 example is not expected to work anymore, so I'm not bothered by that code. But of course, we don't want to destroy people's ability to use the SML standard library, so we should probably try to figure out the right way forward. Execution of our interactive hol command, and the script-files that are executed during theory-building is handled by shell-scripts so it would be trivial to precede the call to buildheap with a

LC_TIME=C

prefix. Other executables that HOL builds but doesn't necessarily control all invocations of would just have to be invoked with that prefix in Holmakefiles that call them. (And other users would just have to know to do it I guess.)