Pedro Abreu (Jun 17 2025 at 15:00): Pedro Abreu (Jun 17 2025 at 15:00):Hi all! :wave:
I'm the host of the Type Theory Forall podcast and website (https://typetheoryforall.com), where I explore topics in type theory, PL, and formal methods through longform interviews and accessible content.
I recently started a small merch shop to help support the project and have begun selling mugs featuring the Rocq logo (with their blessing). I'd love to do something similar with the Isabelle logo—just a simple mug design with the logo on it.
Before moving forward, I wanted to ask: is the Isabelle logo considered open source, or otherwise freely reusable for something like this? If there are any guidelines or restrictions I should follow, I'd be happy to comply.
Thanks in advance!
—Pedro
Fabian Huch (Jun 17 2025 at 15:22):Hi Pedro, that's a good question. In lib/logo there is an index.html which mentions the contributor of the logo, but not much else. Legally, the source code is under BSD-3 license which does not mention trademark, so I would assume that technically the IP lies at the original author, and you'd have to get permission from them (I am not a lawyer).
Practically, I don't think anyone would object, but just to be safe you could ask on the isabelle-users mailing list. Perhaps @Manuel Eberl knows more about the topic?
Manuel Eberl (Jun 17 2025 at 16:30):I have no idea. I made an "illegal" knock-off SVG version of the logo a while ago in the hope that no one will mind (no one did so far).
As far as I know, the original version of the logo was designed by Makarius Wenzel's sister, so I assume she holds the rights to it (as I recall, under German law, the author always retains the rights to their creation but can of course give other people permissions/licences to do things with it).
To what extent the fact that the logo is distributed with Isabelle under BSD-3 licence affects what you may or may not do with it, I have no idea. I simply assumed that it was under BSD-3 licence as well and, more importantly, that no one will cause a fuss about it.
Also note that the thing about it being created by Makarius' sister is something I heard from someone at some point and I vaguely recall other people confirming it, but I never actually did confirm it myself and I don't know if there is any actual evidence that this is the case. It may well just be a myth.
Manuel Eberl (Jun 17 2025 at 16:32):Oh yeah and I do also sell Isabelle logo T-shirts on redbubble.com, with similar disregard for the question of whether or not this is legal. However, I set the profit to 0%, so I don't actually make any money from this.
This is in fact the main reason why I created the SVG logo. The official version simply doesn't look great when you scale it up.
Fabian Huch (Jun 17 2025 at 16:36):Manuel Eberl said:
Also note that the thing about it being created by Makarius' sister is something I heard from someone at some point and I vaguely recall other people confirming it, but I never actually did confirm it myself and I don't know if there is any actual evidence that this is the case. It may well just be a myth.
lib/logo/index.html indeed attributes the logo to Franziska Wenzel.
Pedro Abreu (Jun 18 2025 at 20:52):Well, thanks for the pointer, I think I'll send another request to the mailing list and see if anyone can get in contact with Franziska to see if I can get the permission. Thanks! :)
Last updated: Jun 29 2025 at 20:22 UTC