diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 9509d97d411ef8cc8350a05d638e049fb6945d6c..66115eeb561184dbfc53224a4cde604d8e4f3dc6 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -82,6 +82,13 @@ frontend:
     NIX_DERIVATION: .#frontend
   extends: .build_to_artifacts
 
+stdlib:
+  stage: build
+  needs: [ "theories", "frontend" ]
+  variables:
+    NIX_DERIVATION: .#stdlib
+  extends: .build_to_artifacts
+
 tests:
   stage: tests
   script:
diff --git a/Makefile b/Makefile
index 1453573b640123c7ffa9c7aed0ec3049fe4d4de0..2bdf3009361148a253869f0d5a078b09c4d04716 100644
--- a/Makefile
+++ b/Makefile
@@ -1,67 +1,87 @@
-all:
-	@dune build _build/default/refinedrust.install --display short
-.PHONY: all
+COQ_PATH =	_build/lib/coq/user-contrib
+RUST_TARGET = $(shell rustc -vV | sed -n 's|host: ||p')
+RUST_PATH =	target/$(RUST_TARGET)/release
+
+CASE_STUDIES = case_studies/paper-examples case_studies/tests case_studies/minivec
+
+### Project setup
+setup-nix:
+	rm -f dune-project
+.PHONY: setup-nix
 
-install:
-	@dune install
-.PHONY: install
+setup-dune:
+	echo "(lang dune 3.8)" > dune-project
+.PHONY: setup-dune
 
-uninstall:
-	@dune uninstall
-.PHONY: uninstall
+### generic build targets
+generate_all: generate_stdlib generate_case_studies
+.PHONY: generate_all
 
-clean: clean_all
+clean: clean_case_studies clean_stdlib
 	@dune clean
 .PHONY: clean
 
+all_with_examples: all case_studies.proof
+	dune build --display short
+.PHONY: all_with_examples
+
+### core components
+typesystem:
+	cd theories && dune build --display short
+.PHONY: typesystem
+
 frontend:
-	@cd rr_frontend && ./refinedrust build && ./refinedrust install
+	cd rr_frontend && ./refinedrust build
+.PHONY: frontend
 
-setup-nix:
-	rm -f dune-project
+all: frontend typesystem stdlib.proof
+.PHONY: all
 
-setup-dune:
-	echo "(lang dune 3.8)" > dune-project
+### case studies
+case_studies.proof: typesystem
+case_studies.proof:	$(CASE_STUDIES:=.proof)
+.PHONY: case_studies.proof
 
-CASE_STUDIES = case_studies/paper-examples case_studies/tests case_studies/minivec
+clean_case_studies: $(CASE_STUDIES:=.clean)
+.PHONY: clean_case_studies
 
-%.gen: % phony
-	cd $< && cargo refinedrust
-.PHONY: phony
+generate_case_studies:
+generate_case_studies: $(CASE_STUDIES:=.crate)
+.PHONY: generate_case_studies
 
-%.clean: % phony
-	cd $< && cargo clean
-.PHONY: phony
+case_studies/%.proof:	stdlib.proof case_studies/%.crate
+	cd case_studies/$* && dune build --display short
 
-generate_stdlib:
-	$(MAKE) -C stdlib generate_stdlib
-generate_case_studies: $(addsuffix .gen, $(CASE_STUDIES))
-generate_all: generate_stdlib generate_case_studies
+### stdlib
+stdlib.proof: typesystem generate_stdlib
+	RUST_PATH=$(RUST_PATH) $(MAKE) -C stdlib stdlib.proof
+.PHONY: stdlib.proof
 
 clean_stdlib:
-	$(MAKE) -C stdlib clean_stdlib
-clean_case_studies: $(addsuffix .clean, $(CASE_STUDIES))
-clean_all: clean_case_studies clean_stdlib
-
-.PHONY: generate_all
+	RUST_PATH=$(RUST_PATH) $(MAKE) -C stdlib clean_stdlib
+.PHONY: clean_stdlib
 
-check_generate_all: generate_all
-	git diff --exit-code
-.PHONY: check_generate_all
+generate_stdlib:
+	RUST_PATH=$(RUST_PATH) $(MAKE) -C stdlib generate_stdlib
+.PHONY: generate_stdlib
 
-all_with_examples: frontend generate_all
-	dune build --display short
+### Calling the frontend
+# this adds the path to the built frontend so cargo can find it
+%.crate:	export PATH := $(CURDIR)/rr_frontend/$(RUST_PATH):$(PATH)
+%.crate: %
+	cd $* && cargo refinedrust
 
-builddep-opamfiles: builddep/refinedrust-builddep.opam
-	@true
-.PHONY: builddep-opamfiles
+%.clean: phony
+	cd $* && cargo clean
+.PHONY: phony
 
+### Builddep handling
 # see https://stackoverflow.com/a/649462 for defining multiline strings in Makefiles
 define BUILDDEP_OPAM_BODY
 opam-version: "2.0"
 name: "refinedrust-builddep"
-maintainer: "Lennard Gäher"
-author: "Lennard Gäher"
+maintainer: "RefinedRust contributors"
+author: "RefinedRust contributors"
 homepage: "https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev"
 bug-reports: "https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev"
 synopsis: "---"
@@ -90,20 +110,3 @@ builddep: builddep/refinedrust-builddep.opam
 	@echo "# Installing package $^."
 	@opam install $(OPAMFLAGS) $^
 .PHONY: builddep
-
-DUNE_FILES = $(shell find theories/ -type f -name 'dune')
-
-config:
-	@echo "# Setting default configuration"
-	@cp theories/caesium/config/default_config.v theories/caesium/config/selected_config.v
-.PHONY: config
-
-config-no-align:
-	@echo "# Setting no-align configuration"
-	@cp theories/caesium/config/no_align_config.v theories/caesium/config/selected_config.v
-.PHONY: config-no-align
-
-# Currently, we don't need to do anything special before building RefinedC in opam.
-prepare-install-refinedrust:
-	@true
-.PHONY: prepare-install-refinedrust
diff --git a/README.md b/README.md
index 1f4fbeec1651cd2ef79a1e3ff664d6968efdd66d..7248a06bda74a2e4f5c8c7938269893501e8d436 100644
--- a/README.md
+++ b/README.md
@@ -7,8 +7,9 @@ The Coq implementation of RefinedRust can be found in the `theories` subfolder.
 The frontend implementation can be found in the `rr_frontend` subfolder.
 Case studies and tests can be found in the `case_studies` subfolder.
 Stdlib interfaces (without proofs) can be found in the `stdlib` subfolder.
+Documentation can be found in the `docs` subfolder.
 
-The file `paper_mapping.md` in this repository contains more details on how to map the contents of the RefinedRust paper to this repository.
+The file `docs/paper_mapping.md` contains more details on how to map the contents of the RefinedRust paper to this repository.
 
 ### For the `theories` subfolder:
 * the `caesium` subfolder contains the Radium operational semantics, an adaptation of RefinedC's Caesium semantics.
@@ -62,17 +63,17 @@ opam pin add coq 8.17.1
 opam pin add coq-lambda-rust.dev https://gitlab.mpi-sws.org/lgaeher/lambda-rust.git#rr
 make builddep
 ```
-3. Build the project
+3. Build the Coq implementation of the type system
 ```
-dune build theories
+make setup-dune
+make typesystem
 ```
 
 #### Setup instructions for the frontend:
 1. Make sure that you have a working `rustup`/Rust install. Instructions for setting up Rust can be found on https://rustup.rs/.
 2. Run `./refinedrust build` in `rr_frontend` to build the frontend.
-3. Run `./refinedrust install` in `rr_frontend` to install the frontend.
 
-The last command will install RefinedRust's frontend into Rustup's install directory.
+Optionally, you can install the frontend into your Rust path by also running `./refinedrust install` in `rr_frontend`.
 
 ## Frontend usage
 After installing RefinedRust, it can be invoked through `cargo`, Rust's build system and package manager, by running `cargo refinedrust`.
diff --git a/_CoqProject b/_CoqProject
index 73dbf25095fbea77c38a91db80b40bc4358e6fdb..10ebca6095e27e83ad6474f8b58a571dbacb6884 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,25 +1,21 @@
 -Q _build/default/theories/lithium lithium
 -Q _build/default/theories/caesium caesium
 -Q _build/default/theories/rust_typing refinedrust
+-Q _build/default/case_studies/extra_proofs refinedrust.extra_proofs
+
 # We sometimes want to locally override notation, and there is no good way to do that with scopes.
 -arg -w -arg -notation-overridden
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
 
--Q _build/default/rr_frontend/output/minivec_patched refinedrust.examples.minivec_patched
-
+# case studies
 -Q _build/default/case_studies/tests/output/tests refinedrust.examples.tests
 -Q _build/default/case_studies/paper-examples/output/paper_examples refinedrust.examples.paper_examples
 -Q _build/default/case_studies/minivec/output/minivec refinedrust.examples.minivec
 -Q _build/default/case_studies/evenint/output/evenint refinedrust.examples.evenint
 
-
-
-
--Q _build/default/case_studies/extra_proofs/tests/enums refinedrust.extra_proofs.tests.enums
--Q _build/default/case_studies/extra_proofs/minivec refinedrust.extra_proofs.minivec
-
+# stdlib
 -Q _build/default/stdlib/vec/target/verify/vec stdlib.alloc.vec
 -Q _build/default/stdlib/option/target/verify/option stdlib.option.option
 -Q _build/default/stdlib/alloc/target/verify/alloc stdlib.alloc.alloc
diff --git a/_vimrc_local.vim b/_vimrc_local.vim
deleted file mode 100644
index 43ca75c54a4030ab1d726f99a980a83e338218e9..0000000000000000000000000000000000000000
--- a/_vimrc_local.vim
+++ /dev/null
@@ -1,13 +0,0 @@
-let g:ycm_rust_toolchain_root = '/Users/lennard/.rustup/toolchains/refinedrust'
-
-let g:gutentags_ctags_exclude = [
-      \ '*.git',
-      \ '.git',
-      \ '_build',
-      \ '_opam',
-      \ '.*mypy_cache',
-      \ '*.cache',
-      \ 'rr_frontend/target',
-      \ '*.json',
-      \ '*.toml',
-      \ ]
diff --git a/DEVELOPERS.md b/docs/DEVELOPERS.md
similarity index 88%
rename from DEVELOPERS.md
rename to docs/DEVELOPERS.md
index c8208cd51f3bec05f79f93bddbc4d37076ae75ec..a638d3dd0f4e585fe6f31ab76661d038d42ee656 100644
--- a/DEVELOPERS.md
+++ b/docs/DEVELOPERS.md
@@ -13,6 +13,7 @@ We assume that you have `nix` installed on your system. Setup instructions can b
 To setup the project for development purposes, you can use `nix develop` to enter an interactive subshell containing the tools you will need:
 ```bash
 cd <refinedrust-root-project>
+make setup-nix
 nix develop
 ```
 
@@ -25,6 +26,8 @@ error: experimental Nix feature 'nix-command' is disabled; use ''–extra-experi
 
 All you have to do is enable flakes, see this [NixOS wiki page](https://nixos.wiki/wiki/Flakes) for more details on how to enable flakes permanently.
 
+Note: Make sure that you are not currently in an opam switch with a Coq installation -- this may confuse our build setup.
+
 ### Setup using `opam` and `rustup`
 By following the procedure in the `README.md`, you should have the required setup for development.
 
@@ -60,16 +63,17 @@ Please remember to update this value each time the rust toolchain is updated.
 For Vim, [`YouCompleteMe`](https://github.com/ycm-core/YouCompleteMe) has good support for Rust using `rust-analyzer`.
 Look at its README for instructions on configuring keybinds.
 
-However, by default, it ships its own `rustc` toolchain and sources which are used for completion and which are not updated frequently
-(this is apparently due to `rust-analyzer` having a very unstable API; see https://github.com/ycm-core/YouCompleteMe/issues/4012).
+However, by default, it ships its own `rustc` toolchain and sources which are used for completion and which are not updated frequently.
 This creates problems, because YCM will constantly rebuild the project with its own toolchain (and the build cache will conflict with `cargo build` in the toolchain RefinedRust uses, so it needs to do full rebuilds),
 and you won't get proper autocompletion of `rustc` internals.
 
-To work around this, the `_vimrc_local.vim` file shipped in this project sets the right toolchain (if you have installed `https://github.com/LucHermitte/local_vimrc`), by setting:
+You can fix this by setting by giving the path to the current toolchain explicitly.
+First, get the output of `rustc --print sysroot` and copy it.
+Then, put the following into your vim configuration (if you have a plugin for local configuration like `https://github.com/LucHermitte/local_vimrc`, we recommend putting this into the configuration for this project):
 ```
-let g:ycm_rust_toolchain_root = '/home/[user]/.rustup/toolchains/[current-toolchain]'
+let g:ycm_rust_toolchain_root = '[SYSROOT]'
 ```
-You just have to change the `[user]` to match your setup (sadly, references to `home` by `~/` or `$HOME/` do not seem to be supported), and `[current-toolchain]` to the current version of the RefinedRust toolchain declared in `rust-toolchain.toml`.
+where `SYSROOT` is the output of `rustc --print sysroot`.
 
 To set the `rustc` sources, setup a `.ycm_extra_conf.py` file (for setting it globally, add e.g.
 ```
@@ -104,7 +108,7 @@ Please remember to update this value each time the rust toolchain is updated, by
 ## Updating dependencies
 
 ### Updating the frontend's rustc version
-1. Update the file `rust-toolchain.toml` in `rr_frontend` to the new desired nightly version.
+1. Update the file `rust-toolchain.toml` to the new desired nightly version.
 2. Make the required changes for `nix` (see below).
 3. Try to get the frontend building again.
 
@@ -130,4 +134,4 @@ To update a dependency:
 1. Replace the `sha256` string with the empty string `""`.
 2. For a `coq` dependency, replace the `version` string with the desired `git` commit hash.
 3. Run `nix build` and wait for the error that throws the hash mismatch.
-4. Replace the `sha256` empty string with the hash from the received error. 
+4. Replace the `sha256` empty string with the hash from the received error.
diff --git a/SPEC_FORMAT.md b/docs/SPEC_FORMAT.md
similarity index 100%
rename from SPEC_FORMAT.md
rename to docs/SPEC_FORMAT.md
diff --git a/paper_mapping.md b/docs/paper_mapping.md
similarity index 100%
rename from paper_mapping.md
rename to docs/paper_mapping.md
diff --git a/tutorial.md b/docs/tutorial.md
similarity index 100%
rename from tutorial.md
rename to docs/tutorial.md
diff --git a/flake.nix b/flake.nix
index 8ac5c61dae70a437dcb59563f52e1f6f62821a6a..29e20266317ed0d4b42d09ab1e63a4cc20d86d88 100644
--- a/flake.nix
+++ b/flake.nix
@@ -58,7 +58,7 @@
 
       rust = {
         toolchain = pkgs.fenix.fromToolchainFile {
-          dir = ./rr_frontend;
+          file = ./rust-toolchain.toml;
           sha256 = "sha256-0NR5RJ4nNCMl9ZQDA6eGAyrDWS8fB28xIIS1QGLlOxw=";
         };
 
@@ -155,7 +155,7 @@
 
           preBuild = ''
             dune() { command dune $@ --display=short; }
-            make generate_stdlib 
+            make generate_stdlib
           '';
           useDune = true;
         };
diff --git a/rr_frontend/refinedrust_frontend/src/bin/cargo-refinedrust.rs b/rr_frontend/refinedrust_frontend/src/bin/cargo-refinedrust.rs
index 4aaf00ac2d0b76b65d3b84a06d81317db783a4be..a1404b793a900e6aa042144e593f7b7e191417f8 100644
--- a/rr_frontend/refinedrust_frontend/src/bin/cargo-refinedrust.rs
+++ b/rr_frontend/refinedrust_frontend/src/bin/cargo-refinedrust.rs
@@ -58,8 +58,6 @@ where
         .arg(&command)
         //.args(features)
         .args(args)
-        .env("RUST_TOOLCHAIN", launch::get_rust_toolchain_channel())
-        .env("RUSTUP_TOOLCHAIN", launch::get_rust_toolchain_channel())
         .env("RUSTC", rr_rustc_path)
         .env("RR_CARGO", "")
         .env("CARGO_TARGET_DIR", &cargo_target)
diff --git a/rr_frontend/rrconfig/src/launch.rs b/rr_frontend/rrconfig/src/launch.rs
index d079011f8ecac36ef88d45c97ab52b04165551ea..df06785502c11d18713684c967f7e264049bcf5c 100644
--- a/rr_frontend/rrconfig/src/launch.rs
+++ b/rr_frontend/rrconfig/src/launch.rs
@@ -44,52 +44,3 @@ fn env_prepend_path(name: &str, value: Vec<PathBuf>, cmd: &mut Command) {
         Err(err) => panic!("Error: {err:?}"),
     }
 }
-
-pub fn get_rust_toolchain_channel() -> String {
-    #[derive(Deserialize)]
-    struct RustToolchainFile {
-        toolchain: RustToolchain,
-    }
-
-    #[derive(Deserialize)]
-    struct RustToolchain {
-        channel: String,
-        #[allow(dead_code)]
-        components: Option<Vec<String>>,
-    }
-
-    let content = include_str!("../../rust-toolchain.toml");
-    // Be ready to accept TOML format
-    // See: https://github.com/rust-lang/rustup/pull/2438
-    if content.starts_with("[toolchain]") {
-        let rust_toolchain: RustToolchainFile =
-            toml::from_str(content).expect("failed to parse rust-toolchain.toml file");
-        rust_toolchain.toolchain.channel
-    } else {
-        content.trim().to_string()
-    }
-}
-
-/// Find RefinedRust's sysroot
-pub fn rr_sysroot() -> Option<PathBuf> {
-    match env::var("RUST_SYSROOT") {
-        Ok(prusti_sysroot) => Some(PathBuf::from(prusti_sysroot)),
-        Err(_) => get_sysroot_from_rustup(),
-    }
-}
-
-fn get_sysroot_from_rustup() -> Option<PathBuf> {
-    Command::new("rustup")
-        .arg("run")
-        .arg(get_rust_toolchain_channel())
-        .arg("rustc")
-        .arg("--print")
-        .arg("sysroot")
-        .output()
-        .ok()
-        .and_then(|out| {
-            print!("{}", String::from_utf8(out.stderr).ok().unwrap());
-            String::from_utf8(out.stdout).ok()
-        })
-        .map(|s| PathBuf::from(s.trim().to_owned()))
-}
diff --git a/rr_frontend/rust-toolchain.toml b/rust-toolchain.toml
similarity index 100%
rename from rr_frontend/rust-toolchain.toml
rename to rust-toolchain.toml
diff --git a/stdlib/Makefile b/stdlib/Makefile
index 33cf8dcc88d724781a91563bf6d8d8abd025d338..ba056bba7f5b2277b49ba426952b551092553ac9 100644
--- a/stdlib/Makefile
+++ b/stdlib/Makefile
@@ -1,16 +1,25 @@
-STDLIB = alloc option result spin vec 
+STDLIB = alloc option result spin vec
+
+RUST_TARGET ?= $(shell rustc -vV | sed -n 's|host: ||p')
+RUST_PATH ?=	target/$(RUST_TARGET)/release
+
 
-%.gen: % phony
-	cd $< && cargo refinedrust
-.PHONY: phony
 
-%.clean: % phony
-	cd $< && cargo clean
-.PHONY: phony
 
-generate_stdlib: $(addsuffix .gen, $(STDLIB))
+generate_stdlib: $(STDLIB:=.crate)
 
-clean_stdlib: $(addsuffix .clean, $(STDLIB))
+clean_stdlib: $(STDLIB:=.clean)
 
-stdlib: generate_stdlib
+stdlib.proof:	$(STDLIB:=.proof)
 	dune build --display short
+
+%.proof:	%.crate
+	cd $* && dune build --display short
+
+%.crate:	export PATH := $(CURDIR)/../rr_frontend/$(RUST_PATH):$(PATH)
+%.crate: %
+	cd $* && cargo refinedrust
+
+%.clean: phony
+	cd $* && cargo clean
+.PHONY: phony
diff --git a/stdlib/refinedrust-stdlib.opam b/stdlib/refinedrust-stdlib.opam
index ebe82ff46108eeb579561e8cbf13fcbd6c3f6711..60fe671bf4439e7a478197ea64e30bbcb959d5ea 100644
--- a/stdlib/refinedrust-stdlib.opam
+++ b/stdlib/refinedrust-stdlib.opam
@@ -3,8 +3,8 @@ name: "refinedrust"
 synopsis: "RefinedRust verification framework"
 homepage: "https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev"
 bug-reports: "https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev"
-maintainer: "Lennard Gäher"
-authors: "Lennard Gäher"
+maintainer: "RefinedRust contributors"
+authors: "RefinedRust contributors"
 description: """
 RefinedRust is a prototype framework for verifying safe and unsafe Rust code.
 """
diff --git a/theories/refinedrust.opam b/theories/refinedrust.opam
index 3488ac7ad81ae4a3dc608f98cbd594f51f35907f..e046268fb8566832600d17518ce1e9fafe7845be 100644
--- a/theories/refinedrust.opam
+++ b/theories/refinedrust.opam
@@ -3,8 +3,8 @@ name: "refinedrust"
 synopsis: "RefinedRust verification framework"
 homepage: "https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev"
 bug-reports: "https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev"
-maintainer: "Lennard Gäher"
-authors: "Lennard Gäher"
+maintainer: "RefinedRust contributors"
+authors: "RefinedRust contributors"
 description: """
 RefinedRust is a prototype framework for verifying safe and unsafe Rust code.
 """