Ivory Cadet: Haskell meets LISP

[limeburst]

My first topic on Deskthority. Greetings!

On my way back from work yesterday, I picked up a certain package from Germany at the local post office, ordered nearly a year ago. These long-awaited keycaps were the missing piece to the completion my custom keyboard project, so now I'm happy to share how it all finally turned out!

Ivory Cadet, on my desk at home.

IMG_2924.jpeg (2.67 MiB) Viewed 5633 times

The board has a black TEX aluminum case, black aluminum plate and S60-X PCB from Sentraq. Hollow noise is caught by padding non-slip below the PCB, and stabilizer rattle caught by filling it full of Teflon grease. It has a Cherry MX linear grey switch for the space bar and blacks for the rest of the board. Hardware-wise, it presents itself to me as a solid, reliable keyboard.

Cadet is a keyboard controller for the ATmega32u4 written in Ivory, a Haskell EDSL for safe systems programming. Ivory was designed for implementing high-assurance software for UAVs, but why not put it in a keyboard? Space Cadet was a keyboard used on LISP machine, and in this incarnation, its keycaps go on a board with the controller written in Ivory. Hence my keyboard's name: Ivory Cadet. My academic interest is in software verification and provable correctness, so the logic symbols of the Space Cadet keycaps and the controller implementation language turned out to be a perfect match for me!

The switches were actually a gift from cookie, from when I was translating between Happy for running the HHKB metal sticker GB. Thanks cookie! The keycaps are unmistakably the Space Cadet set from 7bit's Round 6, with small cadet legends. Thanks to 7bit for accommodating my last minute order changes, and of course running the group buy! I couldn't have finished this board without Deskthority, so thank you all.

What next? Cadet still contains some C code, mostly from the Teensy USB stack. I plan to rewrite these into Ivory. Unicode input support for the logic symbols is a priority too. I'll make sure to update progress on this thread. I'd also like to see some more ducks on the board and maybe a hashbang, so I've put in orders for facetsesame's Honey Spherical Extras. Lastly, how do I go about bribing 7bit into running the Space Cadet set with front printed legends for Round 8?

[Menuhin]

Hi limeburst,

Congrats on getting this wonderful key cap set!
If you can collaborate with 7bit to make front printed legends (or with some doubleshot technique?) happen, please do!

[vvp]

Well I do not like the keyboard(*) but I like very much your firmware approach. I was thinking about trying Atom for a keyboard firmware but at the end I chose the most easy way and only ported chrisandreae's firmware. It supports remaps and macros very well so it's good enough.

Do you use standard USB HID Keyboard/Keypad page (0x07) key codes and the generic USB HID keyboard drivers? If so then I guess that your keyboard will emit a macro (like e.g. <pressAlt><Num+>(<hexdigit>)+<releaseAlt>) to generate a unicode code point. Or on linux, one can use Compose key combinations (which is what I do) for all the crazy unicode characters.

Or is there some special standard which emits unicode code points directly to the raw interrupt USB data stream? If so then what kind of driver do you use for the keyboard on the OS side (windows/linux)?

(*) I'm in the Ergodox / Kinesis Advantage camp

[pdc]

Haata has a suggested USB IO protocol for doing things like injecting UTF-8-encoded characters, but as I understand it standard USB works in terms of scan codes not Unicode.

Depending on your OS you can try creating a keycap file or equivalent for converting keypresses to character data. Either way it would be a lot of work—but how cool it would be to have a keyboard with all those crazy logic symbols on it that actually worked as advertised!

[vvp]

Haata has a suggested USB IO protocol for doing things like injecting UTF-8-encoded characters, but as I understand it standard USB works in terms of scan codes not Unicode.

Yes, common keyboards work with scan codes which you can look at in the pdf link I posted in my previous message. Well it contains the codes for an USB keyboard. PS/2 keyboards may have them different.
I also heard about Haata proposal. But that requires also custom keyboard driver. I do not like much an idea of a keyboard which will not work without installing custom keyboard drivers. I was actually asking in hope that there is already a driver and protocol developed for this.

Depending on your OS you can try creating a keycap file or equivalent for converting keypresses to character data. Either way it would be a lot of work—but how cool it would be to have a keyboard with all those crazy logic symbols on it that actually worked as advertised!

You can have this very easily even now with Compose key combinations and macros in the keyboard. Macros needed if you want to have the compose sequences for some characters to be easier (e.g. at a single key press or a chord).

[attheicearcade]

I was thinking about trying Atom for a keyboard firmware

I too have had this thought, but I don't have the time to commit right now unfortunately. Looking forward to seeing your progress limeburst.

[limeburst]

Well I do not like the keyboard(*) but I like very much your firmware approach. I was thinking about trying Atom for a keyboard firmware but at the end I chose the most easy way and only ported chrisandreae's firmware. It supports remaps and macros very well so it's good enough.

Thanks for the praise! I would have definitely considered Atom as well if I had known about it.

Do you use standard USB HID Keyboard/Keypad page (0x07) key codes and the generic USB HID keyboard drivers? If so then I guess that your keyboard will emit a macro (like e.g. <pressAlt><Num+>(<hexdigit>)+<releaseAlt>) to generate a unicode code point. Or on linux, one can use Compose key combinations (which is what I do) for all the crazy unicode characters.

Yes, this is what I'm aiming for in the near future

Haata has a suggested USB IO protocol for doing things like injecting UTF-8-encoded characters, but as I understand it standard USB works in terms of scan codes not Unicode.

I've met HaaTa a few times over IRC before, and it'd be amazing if I can work on something like that together

[zslane]

The name you gave your board is appropriate for another reason too: Ivory was the name of a Symbolics Lisp Machine processor from the late 1980s.

[hbar]

I wonder why I missed this topic so far. While everyone seems to be flattered by your keycaps, I'm more interested in the firmware. Would you mind sharing your Ivory code with us? Just starting out with Ivory, I think I could learn a thing or two from you.

[XMIT]

I wonder why I missed this topic so far. While everyone seems to be flattered by your keycaps, I'm more interested in the firmware. Would you mind sharing your Ivory code with us? Just starting out with Ivory, I think I could learn a thing or two from you.

I thought he did in the OP?

https://github.com/limeburst/cadet

[hbar]

Good Lord, I must be blind. Sorry for that...