• Stars
    star
    114
  • Rank 308,031 (Top 7 %)
  • Language Isabelle
  • License
    Other
  • Created over 10 years ago
  • Updated about 1 month ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

git mirror of the Munich isabelle hg repository
The Isabelle System Distribution
================================

See the NEWS file in the distribution for details on user-relevant
changes.  The ANNOUNCE file recounts notable changes for the latest
official release.

The core of Isabelle is subject to a 3-clause BSD license, but add-on
components have their own license schemes (similar to a Linux
distribution).


Installation
------------

Isabelle works on the three main platform families: Linux, Windows,
and macOS.  The application bundles from the Isabelle web page
include sources, documentation, and add-on tools for all supported
platforms.

Some technical background information may be found in the Isabelle
System Manual (directory doc).


User interface
--------------

Isabelle/jEdit is an advanced Prover IDE based on jEdit and
Isabelle/Scala.  It is the main example application of the
Isabelle/PIDE framework, and the default user interface of
Isabelle.  It provides a metaphor of continuous proof checking of a
versioned collection of theory sources, with instantaneous feedback
in real-time and rich semantic markup associated with the formal
text.


Other sources of information
----------------------------

  * The Isabelle Page

    The Isabelle home page may be accessed from the following mirror
    sites:

     * https://www.cl.cam.ac.uk/research/hvg/Isabelle
     * https://isabelle.in.tum.de
     * https://mirror.cse.unsw.edu.au/pub/isabelle
     * https://mirror.clarkson.edu/isabelle

  * Mailing list

    The electronic mailing list [email protected] provides a
    forum for Isabelle users to discuss problems and exchange
    information.  To join, send a message to
    [email protected].

  * Personal mail

    Lawrence C Paulson
    Computer Laboratory
    University of Cambridge
    JJ Thomson Avenue
    Cambridge CB3 0FD
    England
    E-mail: [email protected]
    Phone: +44-223-763500
    Fax: +44-223-334748

    or

    Tobias Nipkow
    Institut für Informatik
    Technische Universität München
    Boltzmannstr. 3
    D-85748 Garching
    Germany
    E-mail: [email protected]
    Phone: +49-89-289-17302
    Fax: +49-89-289-17307

NOTE:
    Please report any problems you encounter. While we shall try to be
    helpful, we can accept no responsibility for the deficiencies of
    Isabelle and their consequences.

More Repositories

1

seL4

The seL4 microkernel
C
4,718
star
2

l4v

seL4 specification and proofs
Isabelle
510
star
3

rust-sel4

Rust support for seL4 userspace
Rust
117
star
4

microkit

Microkit - A simple operating system framework for the seL4 microkernel
Rust
82
star
5

util_libs

C
55
star
6

seL4_libs

No-assurance libraries for rapid-prototyping of seL4 apps.
C
52
star
7

sel4-tutorials

Tutorials for working with seL4 and/or CAmkES.
Python
52
star
8

refos

Prototype no-assurance reference OS personality built on seL4
C
49
star
9

seL4_tools

Basic tools for building seL4 projects
C
43
star
10

capdl

Capability Distribution Language tools for seL4
Haskell
34
star
11

rumprun-sel4-demoapps

Apps for running with the rumprun unikernel on seL4.
C
29
star
12

camkes-tool

The main CAmkES tool
Python
29
star
13

camkes

Component Architecture test suite and example apps.
C
27
star
14

musllibc

C
25
star
15

sel4test

Test suite for seL4.
C
25
star
16

camkes-vm

Virtual Machine built as a CAmkES component.
C
24
star
17

refos-manifest

Reference Operating system based on seL4 --- example code
21
star
18

camkes-manifest

Top level project for CAmkES, a component platform that provides support for developing and building static seL4 systems as a collection of interacting components.
20
star
19

seL4_projects_libs

C
19
star
20

sel4bench

sel4 benchmarking applications and support library.
C
18
star
21

camkes-vm-examples

C
16
star
22

docs

This is the source of the seL4 docs.
C
16
star
23

verification-manifest

Manifests for the collection of verification repositories
15
star
24

sel4test-manifest

Project to build and test seL4 for many different platforms
14
star
25

seL4-CAmkES-L4v-dockerfiles

Dockerfiles defining the dependencies required to build seL4, CAmkES, and L4v.
Shell
13
star
26

sel4runtime

A minimal runtime for seL4 applications.
C
12
star
27

camkes-arm-vm

C
11
star
28

graph-refine

Python
10
star
29

sel4-tutorials-manifest

8
star
30

camkes-arm-vm-manifest

Manifest for building a virtual machine on seL4 on ARM.
7
star
31

sel4webserver

An seL4 reference webserver application
CMake
7
star
32

sel4bench-manifest

Manifest of the seL4bench project, which contains microbenchmarks for seL4.
6
star
33

camkes-vm-examples-manifest

6
star
34

camkes-vm-manifest

CAmkES code and examples
6
star
35

projects_libs

C++
6
star
36

camkes-vm-linux

CMake
4
star
37

global-components

C
4
star
38

rust-microkit-http-server-demo

Demonstrates the use of the seL4 crates with the seL4 Microkit
Rust
4
star
39

machine_queue

Machine Queue scripts for remote access to our CI system
Shell
4
star
40

website

The seL4.systems website
HTML
3
star
41

ci-actions

CI GitHub actions for the seL4 repositories
Python
3
star
42

rust-microkit-demo

Demonstrates the use of the seL4 crates with the seL4 Microkit
Rust
2
star
43

camkes-vm-images

Precompiled kernels etc. for use with camkes VMs.
CMake
2
star
44

sel4webserver-manifest

2
star
45

pruner

Tool for trimming functions from a C source file
C
2
star
46

rust-root-task-demo

Demonstrates the use of the seL4 crates to construct a simple system
Dockerfile
1
star
47

mcs-examples

Native seL4 and CAmkES examples of mixed criticality mechanisms.
C
1
star
48

cakeml_libs

A collection of libraries and utilities to be used with CakeML applications.
Standard ML
1
star