IsarMathLib version 1.6.5 relased

I have released a new version of IsarMathLib. This time there is some new formalized mathematics related to the theorem that two linearly ordered finite sets with the same number of elements are order-isomorphic and the isomorphism is unique. I have written previously on the motivation for this. The theorem was surprisingly tedious to prove and required about 50 lemmas in a couple of theories. Some corner cases were quite bizarre and kōan-like. For example: what is the order automorphism of the empty set? Turns out the empty set is a function, an injection, surjection, bijection and the only order automorphism of itself.

I found that IsarMathLib is traced on the Ohloh site. Ohloh tries to give various metrics on the code for open source projects that it can find on the web. According to Ohloh, IsarMathLib is written mostly in JavaScript and I am a very lousy JavaScript programmer. I guess this is because of the Tiddly Formal Math site template that is included in the IsarMathLib Subversion repository. They do notice that the project has some Haskell code, but also mention OCaml and this is a complete mystery to me. Isar is not on the list of the languages they support, which is not too surprising. This is funny, but may be I should be concerned? What if I am looking for a job and the HR person finds that my programming style is bad and my code is poorly commented, as Ohloh claims? Will I have a chance to explain?


Tags: , ,

2 Responses to “IsarMathLib version 1.6.5 relased”

  1. Seo Sanghyeon Says:

    I am the one who registered IsarMathLib to Ohloh, sorry if I bothered you. They probably think ROOT.ML is written in OCaml, since, you know, it has .ML extension.

  2. slawekk Says:

    I think it was a good idea to register IsarMathLib. I would have done it myself, if I had known about Ohloh. Maybe one day they will support Isar. I wander if there is a way to straighten up that JavaScript misunderstanding …

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.

%d bloggers like this: