This project aims to produce a minimal exo-kernel named "Pip".
The source code is covered by CeCILL-A licence.
The Pip Development Team is:
- Quentin Bergougnoux quentin.bergougnoux@univ-lille1.fr
- Gilles Grimaud gilles.grimaud@univ-lille1.fr
- Michaël Hauspie michael.hauspie@univ-lille1.fr
- Étienne Helluy Lafont e.helluy-lafont@etudiant.univ-lille1.fr
- Samuel Hym samuel.hym@univ-lille1.fr
- Julien Iguchi-Cartigny julien.iguchi-cartigny@univ-lille1.fr
- Narjes Jomaa narjes.jomaa@univ-lille1.fr
- David Nowak david.nowak@univ-lille1.fr
- Mahieddine Yaker mahieddine.yaker@etudiant.univ-lille1.fr
You can generate the "Getting started" tutorial by invoking "make userguide". The full documentation is generated by invoking "make doc".
The markdown-to-html rendering is performed by Strapdown.js, which is sourced here.
Pip is known to build correctly with this toolchain :
- GCC i386, version 4.7.2
- NASM version 2.11.08
- COQ Proof Assistant version 8.5pl2
- GNU Sed version 4.2.2 (install it on an OSX build host through MacPorts : "gsed")
- grub-mkrescue (for ISO image generation; unnecessary for i386 target though)
- Doxygen version 1.8.10 (for documentation generation)
- stack version 1.2.0.2 (is a cross-platform program for developing Haskell projects)
- QEMU i386 version 2.6.50
You can pass several arguments to make to compile the Pip.
- TARGET=... : destination target (defaults to x86_multiboot)
- PARTITION=... : root partition (defaults to minimal)
- KERNEL_ADDR=0x... : Kernel load address (defaults to 0x100000)
- PARTITION_ADDR=0x... : Partition load address (defaults to 0x700000)
- STACK_ADDR=0x... : Early-boot stack address (defaults to 0x300000)
- mrproper|clean|partition|all|kernel|proof|qemu|grub : Requested build operation
Each partition is located into src/partitions/{architecture}/{partition}.
- Configure the toolchain by copying src/partitions/{architecture}/toolchain.mk.template to src/partitions/{architecture}/toolchain.mk, then edit the latter to your needs.
- You can use the "minimal" partition as a base to develop more elaborated software.
- You can compile the partition by invoking "make" in the partition's directory, or use the "partition" build operation on the top directory (main Makefile).
The kernel is divided into four parts.
- MAL : The Memory Abstraction Layer is used to provide small functions to manipulate the MMU.
- IAL : The Interrupt Abstraction Layer is used to provide small functions to manipulate the interrupt controller (configure, enable, disable...).
- Core : The Pip is the Haskell kernel.
- Boot : The bootstrap code, contained in the Pip's code, is the required C/Assembly code required to boot. It initializes some required hardware, and then boots the Coq kernel.
- _CoqProject is a mandatory configuration file for Coq.
- src/ is the source base directory.
- src/MAL is the Memory Abstraction Layer source folder.
- src/IAL is the Interrupt Abstraction Layer source folder.
- src/core is the Pip source folder.
- src/boot contains the "cbits", i.e the required C and assembly code required to boot the coq kernel.
- src/partitions contains the top-level partitions.
- tools/ contains some scripts and tools that may be useful.
- proof/ contains the Coq proof.
- tests/ contains the test suites.
Pip can already boot on real hardware. If available, the first serial output (COM1) should be used for debugging output. The required configuration is 38400 bauds, 8 bits, no parity, one stop bit. You can also enable automatic line feed and carriage return in Minicom (2.7+) for user-friendly output.
The compilation on Linux should be as easy as to install the i386-elf toolchain as well as the other requirements, and use the Makefile to generate a binary image. Use your favourite package manager to install i386 gcc (gcc-multilib), haskell-stack, QEMU, Coq, NASM, Doxygen and GRUB.
Working OS X versions :
- OSX 10.9.x "Mavericks"
- OSX 10.10.x "Yosemite"
- OSX 10.11.x "El Capitan" / Darwin 15.6.0
- macOS 10.12.x Sierra : see "Compiling on Sierra"
Compilation under Darwin :
- Install MacPorts
- Install git, nasm, qemu, i386-elf-gcc, gsed via MacPorts
- Install CoqIDE from the 8.5pl2 .dmg distribution
- Edit conf/x86_multiboot.conf to suit your i386 toolchain (defaults to i386-elf-)
MacPorts currently doesn't provide a binary release of i386-elf-gcc, and the build requires an older version of Texinfo. We don't have a workaround yet. The only way seems to be :
- Go to the tools/darwin/texinfo directory
- Run "sudo port install" in this directory, installing an older version of Texinfo
- Run "sudo port install i386-elf-gcc" again, and it should be okay
Same thing as Darwin, using pkg instead of MacPorts. You'll need to compile Coq from scratch though.
Note: FreeBSD is still an unsupported build platform.