diff --git a/website/docs/getting-started/installation.mdx b/website/docs/getting-started/installation.mdx index c8a491fe..7fb9470d 100644 --- a/website/docs/getting-started/installation.mdx +++ b/website/docs/getting-started/installation.mdx @@ -5,7 +5,7 @@ sidebar_position: 1 # Installing Caesar -You can install Caesar locally or build a Docker image. +You can download a pre-built Caesar binary or Docker image, or manually build Caesar locally. ```mdx-code-block import CodeBlock from '@theme/CodeBlock'; @@ -20,42 +20,97 @@ import TOCInline from '@theme/TOCInline'; ``` -## Option A: Compiling Locally (Recommended) +## Option A: Download Pre-Built Releases (Recommended) -### Installing Dependencies +### a) Pre-Built Binary + +1. Go to the [latest release on GitHub](https://github.com/moves-rwth/caesar/releases/latest) and download the release for your operating system. + +2. Extract the `caesar` binary from the downloaded archive. + +:::info Additional Steps + + + + + You may have to [release the binary from quarantine](https://support.apple.com/guide/mac-help/mh40616/mac) to allow execution: + ```bash + # Execute in the extracted folder + xattr -d com.apple.quarantine ./caesar + ``` + + + + No additional steps necessary. + + + No additional steps necessary. + + +::: + +### b) Docker Image + +We also provide a Docker image. + +```bash +docker pull ghcr.io/moves-rwth/caesar:latest +``` + +You can use this Docker image just like the `caesar` binary. +To access files from your system you need to mount them as volumes. +For example, if you want to verify a program in `./programs/example.heyvl`, the following command mounts the `./programs/` directory as `/root/caesar/programs/` inside the container and uses `caesar` to verify `example.heyvl`. + +```bash +docker run -it -v $PWD/programs:/root/caesar/programs/ ghcr.io/moves-rwth/caesar:latest /root/caesar/programs/example.heyvl +``` + +## Option B: Compiling Locally + +### a) Build Binary + +#### Installing Dependencies You will need to install some dependencies manually: **Rust:** To install [Rust](https://www.rust-lang.org/), we recommend [installation via rustup](https://rustup.rs/). You might need to restart your terminal after installing Rust. -**Fish Shell**: We write some scripts written in [fish](https://fishshell.com/). - -**Build Tools:** Caesar builds [Z3](https://github.com/Z3Prover/z3) itself, so we need Python and [cmake](https://cmake.org/). +**Build Tools:** Caesar builds [Z3](https://github.com/Z3Prover/z3) itself, so we need [Python](https://www.python.org) and [cmake](https://cmake.org/). -```mdx-code-block - {`# Install Rust via rustup -curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -# Install CMake and fish -brew install cmake fish`} - + + ```bash + # Install Rust via rustup + curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh + # Install Python and CMake + brew install python cmake + ``` + - {`# Install Rust via rustup -curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -# Install CMake, LLVM, clang, and fish -apt-get install cmake llvm-dev libclang-dev clang fish`} - + + ```bash + # Install Rust via rustup + curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh + # Install Python, CMake, LLVM and clang + apt-get install python3 cmake llvm-dev libclang-dev clang + ``` + - We do not have build instructions for Windows at the moment. We recommend that you use WSL and refer to the Debian/Linux instructions. - + + 1. [Follow the instructions](https://rustup.rs/) to install Rust via rustup. + 2. Install Python, CMake and LLVM + ```bash + choco install python cmake llvm + ``` + + -``` -### Compiling Caesar +#### Compiling Caesar Simply run the following, and `caesar` will be available on the command-line. Because this will compile a large number of dependencies, this might take a couple of minutes (especially Z3 takes some time). @@ -76,7 +131,7 @@ tests/zeroconf.heyvl::arp: Verified. tests/zeroconf.heyvl::zeroconf: Verified. ``` -## Option B: Docker +### b) Docker Image We also support building a Docker image. This does not require installing dependencies and will package everything in a Docker image named `caesar`. @@ -87,8 +142,10 @@ cd caesar docker build -t caesar -f docker/Dockerfile . ``` -With the Docker image `caesar` built, you can enter the Docker container and work in there. -The following command also mounts the `./caesar/` directory as `/root/caesar/results/` inside the container. +With the Docker image `caesar` built, you can use it just like the `caesar` binary. +To access files from your system you need to mount them as volumes. +For example, if you want to verify a program in `./programs/example.heyvl`, the following command mounts the `./programs/` directory as `/root/caesar/programs/` inside the container and uses `caesar` to verify `example.heyvl`. + ```bash -docker run -it -v $PWD/results:/root/caesar/results/ caesar /bin/bash -``` \ No newline at end of file +docker run -it -v $PWD/programs:/root/caesar/programs/ caesar /root/caesar/programs/example.heyvl +``` diff --git a/website/src/components/HomepageFeatures/index.js b/website/src/components/HomepageFeatures/index.js index 468029dd..822068a8 100644 --- a/website/src/components/HomepageFeatures/index.js +++ b/website/src/components/HomepageFeatures/index.js @@ -157,16 +157,16 @@ domain List {

🏃 Running Caesar

- After installing Rust, install the caesar binary (c.f. Getting Started): + Download and extract the latest caesar binary (or visit Getting Started for alternative installation options).

- {`git clone git@github.com:moves-rwth/caesar.git -cd caesar -cargo install --path . caesar -caesar tests/domains/lossy_list.heyvl` } +

+ The example from above is included in the Git repository. + After downloading and storing it in examples/lossy_list.heyvl you can try Caesar on it: +

+ {`caesar examples/lossy_list.heyvl` }

- This will run Caesar on the example above (it is included in the Git repository). - Caesar will print: tests/domains/lossy_list.heyvl: Verified. + Caesar will print: examples/lossy_list.heyvl: Verified.