Initial commit

.gitignore

+/target

.gitlab-ci.yml

+.push-zamok: &push-zamok
+  - eval $(ssh-agent -s)
+  - echo "$SSH_PRIVATE_KEY" | tr -d '\r' | ssh-add -
+  - \[ -d ${ZAMOK_SOURCE} \] && 
+        rsync -e "ssh -o StrictHostKeyChecking=no -o UserKnownHostsFile=/dev/null" -rqz ${ZAMOK_SOURCE}/. v-lafeychine@zamok.crans.org:www/skavos/${ZAMOK_TARGET} || true
+
+default:
+  image: vlafeychine/rust
+  interruptible: true
+  cache:
+    paths:
+      - .cache/cargo/
+      - target/
+
+variables:
+  CARGO_HOME: "$CI_PROJECT_DIR/.cache/cargo/"
+  RUSTFLAGS: "-D warnings"
+
+
+stages: [ check, build, tests, docs ]
+
+format:
+  stage: check
+  cache: []
+  script:
+    - cargo deny check
+    - cargo fmt --check
+
+lint:
+  stage: check
+  script:
+    - cargo clippy --all-targets --all-features --no-deps
+
+build:
+  stage: build
+  script:
+    - cargo build
+
+tests:
+  stage: tests
+  variables:
+    CARGO_INCREMENTAL: 0
+    EXCL_ENUM_STRUCT: "^([[:space:]]*)(pub |pub(([[:alpha:]]|[[:space:]]|[:])+) )?(enum|struct) "
+    EXCL_ENUM_FN_STRUCT: "^([[:space:]]*)(pub |pub(([[:alpha:]]|[[:space:]]|[:])+) )?(enum|fn|struct) "
+    EXCL_LINE: "//!|#\\[|use|unreachable!|^\\}|${EXCL_ENUM_STRUCT}"
+    EXCL_START: "${EXCL_ENUM_STRUCT}"
+    EXCL_STOP: "^\\}"
+    EXCL_BR_LINE: "#\\[|assert(_eq)?!|(error|warn|info|debug|trace)!|^[[:space:]]*\\}(,)?$|${EXCL_ENUM_FN_STRUCT}"
+    EXCL_BR_START: "#\\[no_coverage\\]|^mod tests \\{|${EXCL_ENUM_STRUCT}"
+    EXCL_BR_STOP: "^\\}"
+    RUSTDOCFLAGS: "${RUSTFLAGS}"
+    RUSTFLAGS: "-Zprofile -Ccodegen-units=1 -Copt-level=0 -Clink-dead-code -Coverflow-checks=off -Zpanic_abort_tests -Cpanic=abort"
+    ZAMOK_SOURCE: coverage
+    ZAMOK_TARGET: coverage/${CI_COMMIT_REF_SLUG}
+
+  cache:
+    paths:
+      - .cache/cargo/
+
+  script:
+    - cargo test
+    - grcov . -s . -b ./target/debug/ --branch --llvm --ignore-not-existing --excl-line "${EXCL_LINE}" --excl-start "${EXCL_START}" --excl-stop "${EXCL_STOP}" --excl-br-line "${EXCL_BR_LINE}" --excl-br-start "${EXCL_BR_START}" --excl-br-stop "${EXCL_BR_STOP}" --ignore "*cargo*" -t cobertura -o ./coverage_raw.xml &&
+        xsltproc --novalid --output ./coverage.xml ./.gitlab-cov.xsl ./coverage_raw.xml || true
+    - grcov . -s . -b ./target/debug/ --branch --llvm --ignore-not-existing --excl-line "${EXCL_LINE}" --excl-start "${EXCL_START}" --excl-stop "${EXCL_STOP}" --excl-br-line "${EXCL_BR_LINE}" --excl-br-start "${EXCL_BR_START}" --excl-br-stop "${EXCL_BR_STOP}" --ignore "*cargo*" -t lcov -o ./coverage.lcov &&
+        genhtml --branch --no-function-coverage --precision 2 ./coverage.lcov -o ./coverage || true
+    - *push-zamok
+
+  artifacts:
+    reports:
+      coverage_report:
+        coverage_format: cobertura
+        path: ./coverage.xml
+
+  coverage: '/^  branches...: \d+.\d+%/'
+
+
+docs:
+  stage: docs
+  variables:
+    ZAMOK_SOURCE: target/doc
+    ZAMOK_TARGET: doc
+
+  only:
+    refs: [ main ]
+
+  script:
+    - cargo doc --no-deps
+    - *push-zamok
\ No newline at end of file

.gitlab-cov.xsl

+<?xml version="1.0"?>
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
+    <xsl:output method="xml"/>
+
+    <xsl:template match="node() | @*">
+        <xsl:copy>
+            <xsl:apply-templates select="node() | @*"/>
+        </xsl:copy>
+    </xsl:template>
+
+    <xsl:template match="line">
+        <xsl:copy>
+            <xsl:apply-templates select="@*"/>
+            <xsl:attribute name="hits">
+                <xsl:choose>
+                    <xsl:when test="conditions/condition[@coverage='0']">0</xsl:when>
+                    <xsl:when test="@hits='0'">0</xsl:when>
+                    <xsl:otherwise>1</xsl:otherwise>
+                </xsl:choose>
+            </xsl:attribute>
+            <xsl:apply-templates select="node()"/>
+        </xsl:copy>
+    </xsl:template>
+
+</xsl:stylesheet>

.rustfmt.toml

+edition = "2021"
+version = "Two"
+required_version = "1.5.1"
+
+# Enable features
+format_code_in_doc_comments = true
+normalize_doc_attributes = true
+reorder_impl_items = true
+wrap_comments = true
+
+# Set the width of lines
+chain_width = 90
+comment_width = 132
+max_width = 132
+use_small_heuristics = "Max"
+
+# Specific width
+struct_lit_width=18
+struct_variant_width=35
+
+# Import handling
+group_imports = "StdExternalCrate"
+imports_granularity = "Module"
+
+# Stylish choices
+match_block_trailing_comma = true
+overflow_delimited_expr = true

Cargo.lock

+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 3
+
+[[package]]
+name = "skavos"
+version = "0.1.0"

Cargo.toml

+[package]
+name = "skavos"
+description = "Minimal operating system"
+
+edition = "2021"
+license = "GPL-3.0-or-later"
+version = "0.1.0"
+
+authors = [
+    "Vincent Lafeychine",
+    "Balthazar Patiachvili",
+]
+
+[dependencies]
\ No newline at end of file

clippy.toml

+doc-valid-idents = ["SkavOS", ".."]
\ No newline at end of file

deny.toml

+all-features = true
+targets = [
+    { triple = "x86_64-unknown-linux-gnu" },
+]
+
+[advisories]
+notice = "deny"
+unmaintained = "deny"
+unsound = "deny"
+vulnerability = "deny"
+yanked = "deny"
+
+ignore = [
+    # atty: Dependency of `clap` and `colored`
+    "RUSTSEC-2021-0145"
+]
+
+[bans]
+multiple-versions = "deny"
+
+[licenses]
+allow-osi-fsf-free = "both"
+confidence-threshold = 1
+copyleft = "allow"
+default = "deny"
+unlicensed = "deny"
+
+exceptions = [
+    { allow = ["Unicode-DFS-2016"], name = "unicode-ident", version = "*" },
+]
+
+[sources]
+unknown-registry = "deny"

flake.nix

+{
+  inputs = {
+    flake-utils.url = "github:numtide/flake-utils";
+    nixpkgs.url = "nixpkgs/nixos-unstable";
+
+    devshell = {
+      url = "github:numtide/devshell";
+      inputs = {
+        flake-utils.follows = "flake-utils";
+        nixpkgs.follows = "nixpkgs";
+      };
+    };
+
+    rust-overlay = {
+      url = "github:oxalica/rust-overlay";
+      inputs = {
+        flake-utils.follows = "flake-utils";
+        nixpkgs.follows = "nixpkgs";
+      };
+    };
+  };
+
+  outputs = { self, devshell, flake-utils, rust-overlay, nixpkgs }:
+    flake-utils.lib.eachDefaultSystem (system:
+      let
+        overlays = [ devshell.overlay (import rust-overlay) ];
+        pkgs = import nixpkgs { inherit overlays system; };
+        rust = pkgs.rust-bin.nightly.latest;
+      in rec {
+        packages = {
+          default = pkgs.rustPlatform.buildRustPackage {
+            pname = "proost";
+            version = "0.1.0";
+
+            nativeBuildInputs = [ rust.minimal ];
+
+            src = ./.;
+            cargoLock.lockFile = ./Cargo.lock;
+
+            meta = with pkgs.lib; {
+              description = "A simple proof assistant written in Rust";
+              homepage = "https://gitlab.crans.org/loutr/proost";
+              license = licenses.gpl3;
+            };
+          };
+
+          docker-ci = let
+            rust-ci = rust.minimal.override { extensions = [ "clippy" "rustfmt" ]; };
+          in pkgs.dockerTools.buildImage {
+            name = "proost-ci";
+
+            config.Entrypoint = [ "${pkgs.dockerTools.binSh}/bin/sh" "-c" ];
+
+            copyToRoot = pkgs.buildEnv {
+              name = "proost-dependencies";
+              paths = (with pkgs; [ cargo-deny coreutils gcc gnugrep gnused grcov lcov libxslt openssh rsync ])
+                ++ (with pkgs.dockerTools; [ binSh caCertificates fakeNss ]) ++ [ rust-ci ];
+              pathsToLink = [ "/bin" "/etc" ];
+            };
+
+            runAsRoot = "mkdir /tmp";
+          };
+        };
+
+        devShell = let
+          rust-dev = rust.default.override { extensions = [ "rust-src" "rust-analyzer" ]; };
+        in pkgs.devshell.mkShell {
+          name = "proost";
+
+          commands = [{
+            name = "coverage";
+            command = let 
+              excl_enum_struct = "^([[:space:]]*)(pub |pub(([[:alpha:]]|[[:space:]]|[:])+) )?(enum|struct) ";
+              excl_enum_fn_struct = "^([[:space:]]*)(pub |pub(([[:alpha:]]|[[:space:]]|[:])+) )?(enum|fn|struct) ";
+              excl_line = "//!|#\\[|use|unreachable!|^\\}$|${excl_enum_struct}";
+              excl_start = "${excl_enum_struct}";
+              excl_stop = "^\\}$";
+              excl_br_line = "#\\[|assert(_eq)?!|(error|warn|info|debug|trace)!|^[[:space:]]*\\}(,)?$|${excl_enum_fn_struct}";
+              excl_br_start = "#\\[no_coverage\\]|^mod tests \\{|${excl_enum_struct}";
+              excl_br_stop = "^\\}$";
+              env = "CARGO_INCREMENTAL=0"
+                  + " RUSTFLAGS=\"-Zprofile -Ccodegen-units=1 -Copt-level=0 -Clink-dead-code -Coverflow-checks=off -Zpanic_abort_tests -Cpanic=abort\""
+                  + " RUSTDOCFLAGS=\"-Cpanic=abort\"";
+            in ''
+              ${env} cargo test
+              grcov . -s . -b ./target/debug/ --branch --llvm --ignore '*cargo*' --ignore-not-existing \
+                  --excl-line "${excl_line}" --excl-start "${excl_start}" --excl-stop "${excl_stop}" \
+                  --excl-br-line "${excl_br_line}" --excl-br-start "${excl_br_start}" --excl-br-stop "${excl_br_stop}" \
+                  -o ./target/coverage.lcov --log /dev/null || true
+              find target \( -name "*.gcda" -or -name "*.gcno" \) -delete
+              genhtml --branch --no-function-coverage --precision 2 target/coverage.lcov -o coverage
+            '';
+            help = "Launch tests and generate HTML coverage website";
+          }];
+
+          packages = with pkgs; [ cargo-deny grcov lcov rust-dev ];
+        };
+      });
+}

rust-toolchain.toml

+[toolchain]
+channel = "nightly-2023-01-03"
+components = [ "rust-src", "rust-analyzer" ]
+profile = "default"

src/main.rs

+//! Minimal operating system named SkavOS
+
+#![deny(
+    clippy::complexity,
+    clippy::correctness,
+    clippy::nursery,
+    clippy::pedantic,
+    clippy::perf,
+    clippy::restriction,
+    clippy::style,
+    clippy::suspicious
+)]
+#![allow(
+    clippy::arithmetic_side_effects,
+    clippy::blanket_clippy_restriction_lints,
+    clippy::else_if_without_else,
+    clippy::exhaustive_enums,
+    clippy::exhaustive_structs,
+    clippy::implicit_return,
+    clippy::integer_arithmetic,
+    clippy::match_same_arms,
+    clippy::match_wildcard_for_single_variants,
+    clippy::missing_trait_methods,
+    clippy::mod_module_files,
+    clippy::panic_in_result_fn,
+    clippy::pattern_type_mismatch,
+    clippy::separated_literal_suffix,
+    clippy::shadow_reuse,
+    clippy::shadow_unrelated,
+    clippy::unreachable,
+    clippy::wildcard_enum_match_arm
+)]
+#![cfg_attr(
+    test,
+    allow(
+        clippy::assertions_on_result_states,
+        clippy::enum_glob_use,
+        clippy::indexing_slicing,
+        clippy::non_ascii_literal,
+        clippy::too_many_lines,
+        clippy::unwrap_used,
+        clippy::wildcard_imports,
+    )
+)]
+
+const fn main() {}