Needless to say, the first step will be to blink a LED with ChibiOS. So how do we get there?

First things first. Let's download and "install" ChibiOS. Since Bill Grieman has done the heavy lifting, download from his github. I downloaded as a zip, then moved the ChibiOS_ARM library into the library area for Teensy at arduio-1.6.12/hardware/teensy/avr/libraries. Seemed like a good place to put it. Started up Arduino (I'm using 1.6.12) and looked for ChibiOS as an Example. Not there!

A little digging located the problem: The library.properties for ChibiOS_ARM has architecture = sam. Changing "sam" to "*" solves the problem. Just keep in mind that this won't work for other architectures! Restart Arduino and all the ChibiOS_ARM stuff appears.

Bring in Examples -> ChibiOS_ARM -> chBlink. If you attempt to build (Verify) it, you'll get an error having to do with "Compiler generates FPU instructions for a device without an FPU". As near as I can tell, this is a bogus error. In the process of tracking this down, I discovered that the version of core-cm4.h in the ChibiOS area is not the same as that in the Teensy area. Without trying to resolve the problem (and believing that it was an artifact), I removed it by adding "-D__FPU_PRESENT 1U" to the boards.txt file in arduino -1.6.12/hardware/teensy/avr in the 3.6 area.

Change the line (line 25 in my version of boards.txt):

teensy36.build.flags.defs=-D__MK66FX1M0__ -DTEENSYDUINO=131

to read:

teensy36.build.flags.defs=-D__MK66FX1M0__ -DTEENSYDUINO=131 -D__FPU_PRESENT=1U

Now chBlink builds, but there is still a bunch of warnings related to redefing "true". I fixed this with an obvious modification in arduino -1.6.12/hardware/teensy/avr/cores/Teensy3/wiring.h, line 143.

Change the line:

#define true (!false)

to:

#ifndef true
#define true (!false)
#endif // true?

OK! chBlink now builds and runs happily! Changing the timing of the blink duration works as expected.

Let's push our luck and try chBlinkPrint. It should build without problem with the fixes detailed above. Download it to the Teensy 3.6, then start the Serial Monitor and enter any character. The program begins sending the expected data. Woo-hoo!

EDIT: As noted in the comments below, Floating Point does not work, even though things compile just fine with FPU_PRESENT defined. The problem is easy to demonstrate by simply trying to print a floating point value instead of an int in chBlinkPrint. The reason is that CORTEX_HAS_CPU is hard coded to 0 in cmparams.h (line 46). This suppresses the code that saves the floating point registers during a context switch! Here's how to fix it:

Replace the line 46 in arduino -1.6.12/hardware/teensy/avr/libraries/ChiibiOS_ARM/src/utility/cmparms.h:

#define CORTEX_HAS_FPU 0 // WHG

with the following:

#if __FPU_PRESENT == 1
#define CORTEX_HAS_FPU 1 // jkl
#else
#define CORTEX_HAS_FPU 0
#endif // FPU_PRESENT == 1

So far, the floating point tests I've tried using ChibiOS work correctly. But I don't claim to have tested extensively and will be interested in any failures people might find.

Note that all I've said should apply to Teensy 3.5 as well. Just change the 3.5 area of the boards.text file. Since I don't have a 3.5, I can't test it, but I can't see why it wouldn't work.