Ant S. (Jun 17 2026 at 11:17): Ant S. (Jun 17 2026 at 11:17):Hi, I have some fixes (mostly unicode-related) that I wanted to implement in isabelle/jEdit and write a "pull request" for (or the mercurial equivalent). How exactly do I do this? I can copy the source code but I have no clue how contributing to the isabelle codebase seems to work.
https://github.com/seL4/isabelle/blob/master/README_REPOSITORY
I read this but it says nothing about "PR"-like behaviours, especially from someone who has not contributed is the isabelle repository before
Kevin Kappelmann (Jun 17 2026 at 11:45):You typically first discuss the behaviour that you think deserves a change with the community (e.g. on the mailing list or maybe on Zulip for early stage proposals). Many times, it turns out that the reported behaviour works as expected and there's nothing to change.
Then there are owners for each piece of code (documented at the top of the relevant source files and the mercurial history also tells you which persons contributed to the code). Ultimately, you need to get in contact with the relevant owners and see if they approve of your changes.
Ant S. (Jun 17 2026 at 11:46):oooh,
okie, I'll do that
Ant S. (Jun 17 2026 at 11:46):(ty)
Fabian Huch (Jun 17 2026 at 12:01):Also, the Isabelle implementation is not accidental but usually result of many decades of work. So the chances that an outside contribution improves on the existing sources are generally low.
Fabian Huch (Jun 17 2026 at 12:01):Out of curiosity, what are the unicode-related issues you wanted to address?
Ant S. (Jun 17 2026 at 12:11):From this topic:
A few Unicode symbols not yet supported in Isabelle2025 that would be nice to have for mathematical logic purposes:
The corners or “Quine quotes” — ⌜ and ⌝ — U+231C and U+231D. Maybe nice to add the bottom corners U+231E > and U+231F just for completeness/symmetry.
The negated turnstile symbols ⊬ (U+22AC) “Does Not Prove” and ⊭ (U+22AD) “Not True”
The “Left Tack” symbol ⊣ (U+22A3)....
Dunno how useful this is to bring up, but it seems Dr. Paulson also agrees with this:
...I second the request for Quine quotes, which are often used in some branches of logic, and I hope that is a straightforward thing to do. Similarly for the other symbols...
(I can't get zulip's quote system to work with mailing list messages nicely, hence the delay in responding)
This would now be for Isabelle2026 and it would need modifying IsabelleDejaVu*.ttf (which can be found in doc/fonts, and a few other places afaict). As well as etc/symbols to begin with
Fabian Huch (Jun 17 2026 at 12:19):Extending the Isabelle symbols might be a reasonable contribution, but has little to do with unicode and nothing with Isabelle/jEdit (it requires producing proper glyphs for out font).
Ant S. (Jun 17 2026 at 12:21):oh, I see. I thought it would require introducing support in jEdit as well, because modifying etc/symbols (and using a nerd font that supports the symbol) had jEdit throw some runtime exception about unicode (I don't remember the exact name).
Ant S. (Jun 17 2026 at 12:21):Should I start a thread on the mailing list?
Fabian Huch (Jun 17 2026 at 12:27):Ant S. said:
oh, I see. I thought it would require introducing support in jEdit as well, because modifying symbols (and using a nerd font that supports the symbol) had jEdit throw some runtime exception about unicode (I don't remember the exact name).
It would of course need to fit to the existing symbols. See also Admin/isabelle_fonts/README for more background about font compilation.
Fabian Huch (Jun 17 2026 at 12:28):Ant S. said:
Should I start a thread on the mailing list?
As you wrote, there is already one
Ant S. (Jun 17 2026 at 12:31):Isn't that a few months old? I've read mailing lists before but never written to one. Wouldn't "necroposting" would be considered gauche?
Fabian Huch (Jun 17 2026 at 13:05):No, this would be the right place to post a patch file where glyphs and symbols are added.
Ant S. (Jun 17 2026 at 13:07):ok! I'll write up a patchfile and send it in the thread (if I understood you correctly)
Last updated: Jun 26 2026 at 21:20 UTC