Is remote ATP solving server now down?
Boris Schminke <[email protected]> Sat, 21 Feb 2015 11:37:31 +0000
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <CAC-WUu2ibwvyLMYpAogSyjwbOJL=6PFxq-CJPhV-RwKBVV0y7g@mail.gmail.com> |
I try to use "by;" trigger for remote solving. I use this correct article as a test-case: environ begin 1=1; But when I try (in Emacs with Mizar mode) to type by; instead of ; to auto-complete proof I receive the following message: ATP-Unsolved; :: [ATP details] and the details are: HTTP/1.1 200 OK Date: Sat, 21 Feb 2015 11:36:00 GMT Server: Apache/2.2.20 (Ubuntu) Vary: Accept-Encoding Keep-Alive: timeout=5, max=100 Connection: Keep-Alive Transfer-Encoding: chunked Content-Type: text/html; charset=ISO-8859-1 sh: bin5.29.1227/mizf: not found ========== ========== ========== ========== Request took 0s Any ideas? Regards, Boris