Jan de Muijnck-Hughes

345 Followers
237 Following
3K Posts
Lecturer of type-driven approaches to trustworthy-systems (CyberSecurity) at Strathclyde. Professionally interested in PL & FM Methods; socially interested in coffee, politics, music, the outdoors, sci-fi, high fantasy, & much much more! My work doesn’t define me; it is not my identity.
wwwhttps://tyde.systems/
Pronoun’she/his
Locations🇳🇱 🏴󠁧󠁢󠁷󠁬󠁳󠁿 🇬🇧 🇪🇺

For those that like #Dafny, I am working on porting the documentation to a sphinx project. Fortunately, sphinx supports markdown through myST.

Hopefully when I am finished (including PDF generation of the reference doc) we can look at getting it into Dafny itself...

Mwahahaha...

I found a minimal, simple, and 'stable' javascript library to run simple quizzes in the browser. (No need for heavy weight library, that arguably does more than what I need)

Integrating quizzes into Hakyll was/is a pain, and beyond me.

Trouble was how to insert quizzes! Markdown/pandoc/hakyll does not have a native feature to point to a quiz definition, generate the HTML and then insert.

Hakyll's Partial can be used to insert html content (when combined with raw html tag, but the css conflicts between w3pro.css and Simple.css meant the radio buttons disappeared.

So we insert html using an iframe. Next step is to generate the quiz in a preprocessing step from a yaml file using pandoc (or haskell-mustache) and makefiles...

then upgrade the javascript lib to support better structuring of quizzes using html lists. (I probably won't do that...)

Playing around with `mdbook` and CELs `mdbook-quiz`.

I really like the quiz feature, but I am torn with my Hakyll/Haskell based setup.

Fortunately, mdbook-quiz can be spun out as a separate typescript thingy. Unfortunately, my webdev foo is a bit weak, and I am not sure how best to integrate into my existing Hakyll/Pandoc.

I am not sure if that is worth it.

I really want a separate app (`static-quiz`, for example) to generating things.

Anything Bob can do, I cannot do better. But I will try...

Content is currently static, but there is a project from CEL (client side quizzes) that I may want to integrate in future...

I could get the quiz for free using `mdbook` but look at how pretty this is...

It's getting there....

It’s here!

Mechanising Proof: Computing, Risk, & Trust.

It’s second hand, good condition, owners name on it, and some post its in the back cover.

@bentnib Thanks for the recommendation

A little calm before the storm that is return to work and a new semester.
A shop that sells #zines in #edinburgh

Presenting at #types2025, on playing with constructive negation in Idris2 for fun and profit.

Thanks unnamed colleague for the photo!

(Yes I am barefoot).