Simon Felix
Simon Felix
Can repro: UI is locked during "Loading...". (Is the LoadingOverlay a massive CPU hog?)
FYI: We use the Linux JAR, and place the Windows x64 Z3 executable in the same directory. This works fine on Windows when invoking Stainless with `-solvers=smt-z3`.
Out of curiosity: Which IDEs expect 1 tab = 8 spaces? With a cursory review, I found that my tested editors all expect 1 tab = 1 column (EditPlus, Visual...
Yes, that happens in VS (non-code) as well. However, the IDEs I tested use characters, not columns, when interpreting the error message. I.e., when I click on the error "file.scala:10:10",...
Does this happen as well when you use an external solver? I think it's a known issue that internal solvers don't respect the timeout in all cases.
I found that I can remove the following parts of the JAR without negatively impacting the functionality of my hacked Win32-port: - com/ibm/icu/impl/data/icudt59b - lib-bin/libz3.so
Z3 is included twice in the Linux build, once as library, once as external solver.
Yes, it might be an unsupported operation. The model is from Google Meet. I think it is a quantized model. Wasn't aware that tflite supports fewer operations on Windows than...
FYI: In my case, `-i` told me that a machine reboot was required.
My `msstore` source was listed as `https://storeedgefd.dsx.mp.microsoft.com/v9.0`, which returns ``` No HTTP resource was found that matches the request URI 'https://useast.storeedgefd-origin.xbetservices.akadns.net/v9.0'. ``` Don't know how that URL ended up in...