Readme
You can find more about the Pip protokernel at its website.
The source code is covered by CeCILL-A licence.
The Pip Development Team:
- Quentin Bergougnoux [email protected]
- Julien Cartigny [email protected]
- Gilles Grimaud [email protected]
- Michaël Hauspie [email protected]
- Étienne Helluy Lafont [email protected]
- Samuel Hym [email protected]
- Narjes Jomaa [email protected]
- David Nowak [email protected]
- Paolo Torrini [email protected]
- Mahieddine Yaker [email protected]
Getting started
You can generate the "Getting Started" tutorial by invoking make gettingstarted
. The full documentation is generated by invoking make doc
.
Dependencies
Pip is known to build correctly with this toolchain:
- COQ Proof Assistant version 8.13.1
- Doxygen version 1.8.13 and above (for documentation generation)
- GCC version 8.3.0 and above
- GDB version 8.2.1 and above
- GNU Make version 4.3 and above
- grub-mkrescue (for ISO image generation; unnecessary for i386 target though)
- haskell-stack version 1.7.1 and above (is a cross-platform program for developing Haskell projects)
- NASM version 2.14 and above
- QEMU i386 version 3.1.0 and above
- Texlive any version or another latex tools
Building the Pip
You can pass several arguments to make to compile the Pip.
all
: Build targetproofs
: Proofs targetqemu-elf
|qemu-iso
: QEMU targetsdoc
|doc-c
|doc-coq
|gettingstarted
: Documentation targetstoolchain.mk
: Configure script targetclean
|realclean
: Clean targets
Building partitions
Each partition is located into src/arch/{architecture}/partitions/{partition}
- Configure the toolchain by copying
src/partitions/{architecture}/toolchain.mk.template
tosrc/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.
Kernel structure
The kernel is divided into three parts.
- MAL: The Memory Abstraction Layer is used to provide small functions to manipulate the MMU
- Core: The logic of Pip
- Boot: The bootstrap code that initializes required hardware and then boots Pip
Source code structure
_CoqProject
is a mandatory configuration file for Coq.src/
contains the source base directory.src/core
contains the Pip source folder.src/extraction
contains the code to extract Coq services.src/interface
contains the interface between Coq and C.src/model
contains the Coq code.src/arch/x86_multiboot/MAL
contains the Memory Abstraction Layer source.src/arch/x86_multiboot/boot
contains the "cbits", i.e the required C and assembly code required to boot the coq kernel.src/arch/x86_multiboot/partitions
contains the top-level partitions.tools/
contains some scripts and tools that may be useful.proof/
contains the Coq proof.
Serial configuration
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.
Compiling on Linux
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 Coq, Doxygen, GCC, GDB, GNU Make, GRUB, haskell-stack, NASM, QEMU and Texlive.