[isabelle-dev] Build error (isabelle.Build not found)
Hi all, I just updated Isabelle to af8ecf09a58c (from a version that was one or two days old) and whenever I try to build HOL, I get this error: isabelle build -c -b HOL Fehler: Hauptklasse isabelle.Build konnte nicht gefunden oder geladen werden 0:00:00 elapsed time, 0:00:00 cpu time Mac OS X 10.6. I haven't changed any settings recently. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Build error (isabelle.Build not found)
Am 10.01.2013 um 13:16 schrieb Jasmin Blanchette: I just updated Isabelle to af8ecf09a58c (from a version that was one or two days old) and whenever I try to build HOL, I get this error: isabelle build -c -b HOL Fehler: Hauptklasse isabelle.Build konnte nicht gefunden oder geladen werden 0:00:00 elapsed time, 0:00:00 cpu time Mac OS X 10.6. I haven't changed any settings recently. I did some updates back and forth along the history and strangely enough the problem disappeared once I went back to the above change (af8ecf09a58c). Strange. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Build error (isabelle.Build not found)
On 01/10/2013 01:25 PM, Jasmin Christian Blanchette wrote: Am 10.01.2013 um 13:16 schrieb Jasmin Blanchette: I just updated Isabelle to af8ecf09a58c (from a version that was one or two days old) and whenever I try to build HOL, I get this error: isabelle build -c -b HOL Fehler: Hauptklasse isabelle.Build konnte nicht gefunden oder geladen werden 0:00:00 elapsed time, 0:00:00 cpu time Mac OS X 10.6. I haven't changed any settings recently. I did some updates back and forth along the history and strangely enough the problem disappeared once I went back to the above change (af8ecf09a58c). Strange. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev I believe you have the same problem that was already discussed here: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-January/003736.html Ondrej ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] JEdit: type constraints no longer printed by default
In af8ecf09a58c, type constraints are no longer printed by default in JEdit:
ML {*
@{term f}
| Type.constraint @{typ nat = nat}
| Syntax.string_of_term @{context}
| writeln
*}
# f
Is this the intended behaviour? It used to be different a couple of month ago.
I don't know when it changed exacyly, but I think changeset a6814de45b69 might
be responsible for the change.
When setting show_markup to false, the behaviour is like it was in the past:
ML {*
@{term f}
| Type.constraint @{typ nat = nat}
| Syntax.string_of_term (@{context} | Config.put show_markup false)
| writeln
*}
# f∷nat ⇒ nat
Regards,
Steffen___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Pushing to testboard fails
Hi, I just tried pushing some commit to the testboard (via ssh://nosch...@lxbroy10.informatik.tu-muenchen.de//home/isabelle-repository/repos/testboard ) and it failed with: hg push -f testboard pushing to ssh://nosch...@lxbroy10.informatik.tu-muenchen.de//home/isabelle-repository/repos/testboard searching for changes remote: abort: could not lock repository /home/isabelle-repository/repos/testboard: Permission denied abort: unexpected response: empty string Is this still the right URL? Or is something broken on the server side? -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
