From 38647a38741307a11a0047252b7d24efe7980ced Mon Sep 17 00:00:00 2001 From: Jan Baudisch Date: Fri, 3 May 2024 00:38:44 +0200 Subject: [PATCH] feat: enable nix build --- .dockerignore | 18 --- .github/workflows/CI.yaml | 47 ++++++ .github/workflows/Container.yaml | 29 ++++ .github/workflows/{CI.yml => Windows.yaml} | 83 +++------- Cargo.toml | 1 - Dockerfile | 41 ----- README.md | 92 ++++++----- clean.sh | 55 ------- ddnnife_dw.sh | 26 ---- doc/aarch64-darwin-d4.md | 1 + doc/aarch64-darwin.md | 1 + doc/built/macos.md | 1 - doc/{built => }/windows-d4.md | 0 doc/{built => }/windows.md | 0 .../macos-d4.md => x86_64-darwin-d4.md} | 22 +-- doc/x86_64-darwin.md | 1 + doc/{built/linux-d4.md => x86_64-linux-d4.md} | 17 +-- doc/{built/linux.md => x86_64-linux.md} | 0 flake.lock | 130 ++++++++++++++++ flake.nix | 144 ++++++++++++++++++ 20 files changed, 440 insertions(+), 269 deletions(-) delete mode 100644 .dockerignore create mode 100644 .github/workflows/CI.yaml create mode 100644 .github/workflows/Container.yaml rename .github/workflows/{CI.yml => Windows.yaml} (56%) delete mode 100644 Dockerfile delete mode 100755 clean.sh delete mode 100755 ddnnife_dw.sh create mode 120000 doc/aarch64-darwin-d4.md create mode 120000 doc/aarch64-darwin.md delete mode 120000 doc/built/macos.md rename doc/{built => }/windows-d4.md (100%) rename doc/{built => }/windows.md (100%) rename doc/{built/macos-d4.md => x86_64-darwin-d4.md} (55%) create mode 120000 doc/x86_64-darwin.md rename doc/{built/linux-d4.md => x86_64-linux-d4.md} (58%) rename doc/{built/linux.md => x86_64-linux.md} (100%) create mode 100644 flake.lock create mode 100644 flake.nix diff --git a/.dockerignore b/.dockerignore deleted file mode 100644 index 7f052a5..0000000 --- a/.dockerignore +++ /dev/null @@ -1,18 +0,0 @@ -# ignore everything -* - -# besides source code, build script and dependency data -!src/ -!build.rs -!Cargo.toml -!Cargo.lock - -#d4v2 -#mermaid-transfer/ -#target/ -#valcom/ -#complete_exa/ -#.vscode/ -#.github/ -#.gitignore -#tests/ \ No newline at end of file diff --git a/.github/workflows/CI.yaml b/.github/workflows/CI.yaml new file mode 100644 index 0000000..33f0abf --- /dev/null +++ b/.github/workflows/CI.yaml @@ -0,0 +1,47 @@ +name: CI + +on: + - push + +jobs: + Lint: + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v4 + - name: Nix + uses: DeterminateSystems/nix-installer-action@v10 + - name: Cache + uses: DeterminateSystems/magic-nix-cache-action@v4 + - name: Check + run: nix flake check -L + + Build: + strategy: + fail-fast: false + matrix: + target: + - triple: x86_64-unknown-linux-gnu + runner: ubuntu-latest + - triple: x86_64-apple-darwin + runner: macos-13 + - triple: aarch64-apple-darwin + runner: macos-latest + variant: + - '' + - '-d4' + runs-on: ${{ matrix.target.runner }} + steps: + - name: Checkout + uses: actions/checkout@v4 + - name: Nix + uses: DeterminateSystems/nix-installer-action@v10 + - name: Cache + uses: DeterminateSystems/magic-nix-cache-action@v4 + - name: Build + run: nix build -L .#bundled${{ matrix.variant }} + - name: Upload + uses: actions/upload-artifact@v4 + with: + name: ddnnife-${{ matrix.target.triple }}${{ matrix.variant }} + path: result diff --git a/.github/workflows/Container.yaml b/.github/workflows/Container.yaml new file mode 100644 index 0000000..42110ee --- /dev/null +++ b/.github/workflows/Container.yaml @@ -0,0 +1,29 @@ +name: Container + +on: + - push + +env: + REGISTRY: ghcr.io + IMAGE_NAME: softvare-group/ddnnife + TAG: ${{ github.ref_name }} + +jobs: + Build: + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v4 + - name: Nix + uses: DeterminateSystems/nix-installer-action@v10 + - name: Cache + uses: DeterminateSystems/magic-nix-cache-action@v4 + - name: Build + run: nix build -L .#container + - name: Login + run: nix run nixpkgs#skopeo -- login $REGISTRY --username ${{ github.actor }} --password ${{ secrets.GITHUB_TOKEN }} + - name: Push + run: nix run nixpkgs#skopeo -- copy docker-archive:result docker://$REGISTRY/$IMAGE_NAME:$TAG + - name: Push latest tag + if: ${{ github.ref_type == 'tag' }} + run: nix run nixpkgs#skopeo -- copy docker://$REGISTRY/$IMAGE_NAME:$TAG docker://$REGISTRY/$IMAGE_NAME:latest diff --git a/.github/workflows/CI.yml b/.github/workflows/Windows.yaml similarity index 56% rename from .github/workflows/CI.yml rename to .github/workflows/Windows.yaml index 1b9079b..7453668 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/Windows.yaml @@ -1,6 +1,7 @@ -name: CI +name: Windows -on: [workflow_dispatch, push] +on: + - push env: CARGO_TERM_COLOR: always @@ -9,66 +10,36 @@ env: CMAKE_CXX_COMPILER_LAUNCHER: sccache RUSTC_WRAPPER: sccache SCCACHE_GHA_ENABLED: true - # FIXME: cc-rs on mac currently won't set the C++ standard correctly (https://github.com/dtolnay/cxx/issues/1217). - CXXFLAGS: -std=c++17 jobs: - Format: - runs-on: ubuntu-latest - steps: - - name: Checkout - uses: actions/checkout@v4 - - name: Format - run: cargo fmt --check - Build: strategy: fail-fast: false matrix: target: - - os: linux - runner: ubuntu-latest - triple: x86_64-unknown-linux-gnu - shell: bash - coverage: true - - os: macos - runner: macos-latest - triple: x86_64-apple-darwin - shell: bash - - os: windows - runner: windows-latest - triple: x86_64-pc-windows-gnu - shell: msys2 + - triple: x86_64-pc-windows-gnu msystem: ucrt64 toolchain: - stable d4: - include - exclude - runs-on: ${{ matrix.target.runner }} + runs-on: windows-latest defaults: run: - shell: ${{ matrix.target.shell }} {0} + shell: msys2 {0} env: CARGO_BUILD_TARGET: ${{ matrix.target.triple }} steps: - name: Checkout uses: actions/checkout@v4 - - name: Setup MSYS2 (Windows) - if: ${{ matrix.target.os == 'windows' }} + - name: Setup MSYS2 uses: msys2/setup-msys2@v2 with: path-type: inherit - msystem: ${{ matrix.target.msystem }} + msystem: ucrt64 pacboy: git m4 cmake:p ninja:p - - name: Install dependencies (Linux) - if: ${{ matrix.target.os == 'linux' }} - run: sudo apt-get install ninja-build libtbb-dev libhwloc-dev libboost-program-options-dev - - name: Install dependencies (macOS) - if: ${{ matrix.target.os == 'macos' }} - run: brew install ninja boost hwloc tbb - - name: Install dependencies (Windows) - if: ${{ matrix.target.os == 'windows' }} + - name: Install dependencies run: | pacboy -S --noconfirm toolchain:p tbb:p hwloc:p boost:p mv /${{ matrix.target.msystem }}/lib/libtbb12.dll.a /${{ matrix.target.msystem }}/lib/libtbb.dll.a @@ -91,54 +62,36 @@ jobs: run: | cd $(mktemp -d) git clone --recursive https://github.com/kahypar/mt-kahypar.git . + git checkout c51ffeaa3b1040530bf821b7f323e3790b147b33 cmake -B build -D CMAKE_INSTALL_PREFIX=$BUILD_ROOT -D MT_KAHYPAR_DISABLE_BOOST=true cmake --build build --target mtkahypar cmake --install build - mkdir -p $BUILD_ROOT/licenses/mt-kahypar - cp LICENSE $BUILD_ROOT/licenses/mt-kahypar/ -# TODO: currently, macOS is only supported on master, move below clone to check out latest version when released. -# git checkout $(git describe --tags $(git rev-list --tags --max-count=1)) - name: Build (including d4) if: ${{ matrix.d4 == 'include' }} run: cargo build - name: Build (excluding d4) if: ${{ matrix.d4 == 'exclude' }} run: cargo build --no-default-features - - name: Test - # FIXME: Some tests are currently not platform independent and fail on macos and windows and without d4 - if: ${{ matrix.d4 == 'include' && matrix.target.os != 'macos' && matrix.target.os != 'windows' }} - run: cargo test - - name: Install coverage tool - if: ${{ matrix.target.coverage }} - uses: taiki-e/install-action@cargo-llvm-cov - - name: Coverage - if: ${{ matrix.target.coverage && matrix.d4 == 'include' }} - run: cargo llvm-cov - name: Package run: | mkdir -p $BUILD_ROOT/bin cp target/${{ matrix.target.triple }}/debug/{ddnnife,dhone} $BUILD_ROOT/bin/ + ./package-msys.bash $BUILD_ROOT $BUILD_ROOT/bin/* rm -rf $BUILD_ROOT/include rm -rf $BUILD_ROOT/share - mkdir -p $BUILD_ROOT/licenses/d-ddnnf-reasoner - cp LICENSE $BUILD_ROOT/licenses/d-ddnnf-reasoner/ + rm -f $BUILD_ROOT/bin/b2 + rm -f $BUILD_ROOT/bin/bjam + rm -f $BUILD_ROOT/bin/hwloc* + rm -f $BUILD_ROOT/bin/lstopo* + rm -rf $BUILD_ROOT/lib - name: Package documentation (including d4) if: ${{ matrix.d4 == 'include' }} run: | - cp doc/built/${{ matrix.target.os }}-d4.md $BUILD_ROOT/README.md + cp doc/windows-d4.md $BUILD_ROOT/README.md - name: Package documentation (excluding d4) if: ${{ matrix.d4 == 'exclude' }} run: | - cp doc/built/${{ matrix.target.os }}.md $BUILD_ROOT/README.md - - name: Package dependencies (Windows) - if: ${{ matrix.target.os == 'windows' }} - run: | - ./package-msys.bash $BUILD_ROOT $BUILD_ROOT/bin/* - rm -f $BUILD_ROOT/bin/b2 - rm -f $BUILD_ROOT/bin/bjam - rm -f $BUILD_ROOT/bin/hwloc* - rm -f $BUILD_ROOT/bin/lstopo* - rm -rf $BUILD_ROOT/lib + cp doc/windows.md $BUILD_ROOT/README.md - name: Upload (including d4) if: ${{ matrix.d4 == 'include' }} uses: actions/upload-artifact@v4 diff --git a/Cargo.toml b/Cargo.toml index 90a682b..ac081c4 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -23,7 +23,6 @@ codegen-units = 1 # for performance graphs: debug = true [features] -default = ["d4"] d4 = ["dep:d4-oxide"] [dependencies] diff --git a/Dockerfile b/Dockerfile deleted file mode 100644 index 28142db..0000000 --- a/Dockerfile +++ /dev/null @@ -1,41 +0,0 @@ -FROM ubuntu:latest as builder -# We NEED that line! -# Otherwise, cargo has a tantrum, finds an infinite amount of file system loops, and hangs itself :'D -WORKDIR /reasoner - -# Update default packages -RUN apt-get -qq update - -# packages for later installing cargo -RUN apt-get install -y -q build-essential curl - -# gmp -RUN apt-get install -y -q libgmp-dev m4 diffutils gcc make - -# d4v2 -RUN apt-get install -y -q ninja-build git libz-dev cmake libboost-all-dev - -# Get Rust; NOTE: using sh for better compatibility with other base images -RUN curl https://sh.rustup.rs -sSf | sh -s -- -y - -# Add .cargo/bin to PATH -ENV PATH="/root/.cargo/bin:${PATH}" - -COPY ./ ./ - -# Build d4v2 in an extra step outside of the build script to allow for better caching -# while building the image. Running the build script of d4v2 is very labor-intensive. -RUN mkdir d4v2 -RUN git clone https://github.com/SoftVarE-Group/d4v2.git d4v2/. -WORKDIR /reasoner/d4v2 -RUN ./build.sh - -RUN cargo build --release -WORKDIR /reasoner -RUN cp ./target/release/ddnnife ./ - -# Move the binary in an enviroment that is smaller in size, saving around 2/3 of the size -FROM frolvlad/alpine-glibc -COPY --from=builder /reasoner/ddnnife ./ddnnife -RUN apk add gmp-dev -ENTRYPOINT ["./ddnnife"] \ No newline at end of file diff --git a/README.md b/README.md index da4ae7b..8d912a5 100644 --- a/README.md +++ b/README.md @@ -20,14 +20,63 @@ Additionally, via the stream API, it can compute SAT queries, core/dead features # Installation +## Pre-built + You can use pre-built binaries for Linux, macOS or Windows. There are two flavours for each target, one with the d4 compiler included and one without. Builds for the latest release are attached as assets for each [release][releases]. Using the variant without d4 is straight forward, there are no external dependencies. -The variant with d4 has some dynamic dependencies which need to be installed. +The variant with d4 has some dynamic dependencies which need to be set up. Please see the README inside the release folder for details. +### Nix + +This project can be used and developed via a [Nix][nix] [flake][flake]. + +With Nix installed simply run the following for a build: + +``` +nix build +``` + +The result will be at `result`. + +To build without the need to clone the repository, use: + +``` +nix build github:SoftVarE-Group/d-dnnf-reasoner +``` + +The default package output (`ddnnife-d4`) includes `d4`. +To build the variant without `d4` use the package `ddnnife`: + +``` +nix build .#ddnnife +``` + +## Container + +There is also a container image for usage with [Docker][docker], [Podman][podman] or any other container tool. + +For an overview, see [here][container]. + +There is a tag for each branch and for each tagged release. +Currently, the latest version is found on the `main` branch. +To pull the container, use: + +``` +docker pull ghcr.io/softvare-group/ddnnife:main +``` + +Then, you can use it like the standalone binary. +For `ddnnife` to be able to access files, you need to create a volume. +The following mounts `` on `/work` inside the container: + +``` +docker run -v :/work ddnnife:main /work/ count +``` + # Building ## Requirements @@ -362,42 +411,6 @@ To generate an HTML documentation of the code and open it in the default browser cargo doc --open ``` -# Container - -If you want to, you can also use a container image. -However, we recommend using the native binary if possible. - -## Build - -You can either use the provided script in the following way to build the image and also interact with it - -``` -./ddnnife_dw.sh -``` - -or you can build the image directly by hand. -Here, ```ddnnife``` is the name of the image. - -``` -docker build -t ddnnife . -``` - -## Usage - -Like in the previous section you can use `./ddnnife_dw.sh` to interact with the image, or you can do the same by hand in with the following command: - -``` -docker run --platform linux/amd64 -i --rm -v [HOST FOLDER ABSOLUTE]:/data ddnnife -``` - -```--platform linux/amd64``` is necessary for host systems that are not ```linux x_86```, ```-i``` keeps STDIN open (which is relevant for the stream API), ```--rm``` removes the used container, and ```-v``` adds a volume to the container. [HOST FOLDER ABSOLUTE] is the folder on the host system that contains the input files for ```ddnnife```. ```ddnnife``` is the name of the image we created in the previous step. - -After that arguments for ```ddnnife``` can be passed. It is important that to access the files mounted via the volume, you need to add the ```/data/``` prefix to all the input and output files. An example to compute the cardinality of features for ```auto1``` can look like the following. - -``` -docker run --platform linux/amd64 -i --rm -v ~/Documents/d-dnnf-reasoner/example_input:/data ddnnife /data/auto1.cnf count-features /data/result -``` - [releases]: https://github.com/SoftVarE-Group/d-dnnf-reasoner/releases [c2d]: http://reasoning.cs.ucla.edu/c2d [d4]: https://github.com/SoftVarE-Group/d4v2 @@ -407,3 +420,8 @@ docker run --platform linux/amd64 -i --rm -v ~/Documents/d-dnnf-reasoner/example [mtkahypar]: https://github.com/kahypar/mt-kahypar [msys2]: https://msys2.org [llvm-cov]: https://github.com/taiki-e/cargo-llvm-cov +[nix]: https://nixos.org +[flake]: https://nixos.wiki/wiki/Flakes +[docker]: https://docker.com +[podman]: https://podman.io +[container]: https://github.com/SoftVarE-Group/d-dnnf-reasoner/pkgs/container/ddnnife diff --git a/clean.sh b/clean.sh deleted file mode 100755 index e25990e..0000000 --- a/clean.sh +++ /dev/null @@ -1,55 +0,0 @@ -#!/bin/bash - -if [ $# -eq 0 ] -then - echo "USAGE: sh clean-all.sh [FILES TO CLEAR]" - echo -e "\t0: All of the below" - echo -e "\t1: Target directory" - echo -e "\t2: d4v2 related files" - echo -e "\t3: ddnnife results" - echo -e "\t4: ddnnife image" - exit 0 -fi - -# target directory -if [ $1 -eq 0 ] || [ $1 -eq 1 ] -then - echo "Removing the target directory..." - cargo clean -fi - -# d4v2 related files -if [ $1 -eq 0 ] || [ $1 -eq 2 ] -then - echo "Removing d4v2 related files..." - rm -rf d4v2 - rm src/parser/d4v2.bin 2> /dev/null - rm src/bin/d4v2.bin 2> /dev/null -fi - -if [ $1 -eq 0 ] || [ $1 -eq 3 ] -then - echo "Removing ddnnife result files..." - rm *-features.csv \ - *-queries.csv \ - *-sat.csv \ - *-atomic.csv \ - *-wise.csv \ - *-urs.csv \ - *-stream.csv \ - *-core.csv \ - *-anomalies.txt \ - *-saved.nnf \ - *-mermaid.md \ - *.config \ - tarpaulin-report.html \ - out.txt \ - out.nnf \ - out.csv 2> /dev/null -fi - -if [ $1 -eq 0 ] || [ $1 -eq 4 ] -then - echo "Removing ddnnife image..." - docker image rm ddnnife &> /dev/null -fi \ No newline at end of file diff --git a/ddnnife_dw.sh b/ddnnife_dw.sh deleted file mode 100755 index 75c2414..0000000 --- a/ddnnife_dw.sh +++ /dev/null @@ -1,26 +0,0 @@ -#!/bin/bash -# A script to wrap the docker container. -# This simplifies the usage, due to hidding the building of the image and execution of the container. -# Further, verbose parameters such as adding a volume are hidden, resulting in easier accesibility for the user. - -if [ $# -eq 0 ] -then - echo "USAGE: ./ddnnife_dw.sh " - echo -e "\trebuild: Rebuilds the docker image if there already exists one." - echo -e "\t[VOLUME FOLDER]: The folder and its files that should be available to the container." - echo -e "\tExample: ./ddnnife_dw.sh example_input internal/auto1.cnf count-features internal/res" - exit 0 -fi - -if [[ "$(docker images -q ddnnife 2> /dev/null)" == "" ]] || [ "$1" == "rebuild" ] -then - echo -e "Building the docker image. Make sure that the current folder contains ddnnife as well as its Dockerfile...\n" - docker build --platform linux/amd64 -t ddnnife . -fi - -if [ "$1" == "rebuild" ] -then - exit 0 -fi - -docker run --platform linux/amd64 -it --rm -v $(cd "$(dirname "$1")"; pwd)/$(basename "$1"):/internal ddnnife ${@:2} \ No newline at end of file diff --git a/doc/aarch64-darwin-d4.md b/doc/aarch64-darwin-d4.md new file mode 120000 index 0000000..41ad742 --- /dev/null +++ b/doc/aarch64-darwin-d4.md @@ -0,0 +1 @@ +x86_64-darwin-d4.md \ No newline at end of file diff --git a/doc/aarch64-darwin.md b/doc/aarch64-darwin.md new file mode 120000 index 0000000..dcd1e00 --- /dev/null +++ b/doc/aarch64-darwin.md @@ -0,0 +1 @@ +x86_64-darwin.md \ No newline at end of file diff --git a/doc/built/macos.md b/doc/built/macos.md deleted file mode 120000 index dba520c..0000000 --- a/doc/built/macos.md +++ /dev/null @@ -1 +0,0 @@ -linux.md \ No newline at end of file diff --git a/doc/built/windows-d4.md b/doc/windows-d4.md similarity index 100% rename from doc/built/windows-d4.md rename to doc/windows-d4.md diff --git a/doc/built/windows.md b/doc/windows.md similarity index 100% rename from doc/built/windows.md rename to doc/windows.md diff --git a/doc/built/macos-d4.md b/doc/x86_64-darwin-d4.md similarity index 55% rename from doc/built/macos-d4.md rename to doc/x86_64-darwin-d4.md index 5b73d04..1241202 100644 --- a/doc/built/macos-d4.md +++ b/doc/x86_64-darwin-d4.md @@ -5,30 +5,24 @@ The project is licensed under the LGPL-3.0 and the source can be found at https: ## Dependencies -The Mt-KaHyPar dependency is bundled with this build, other dependencies have to be installed: - -- TBB (https://github.com/oneapi-src/oneTBB) -- hwloc (https://open-mpi.org/projects/hwloc) +All dependencies are bundled with this build inside the `lib` directory. +To use the binaries, they have to be visible to the linker. +This can either be accomplished by moving the `lib` directories contents to the global library path (such as `/usr/lib`) +or by setting the `DYLD_LIBRARY_PATH` environment variable to include the `lib` directory. ## Gatekeeper The execution of downloaded binaries might be blocked by Gatekeeper. -To resolve this, the attribute `com.apple.quarantine` has to be removed from `bin/ddnife`, `bin/dhone` and `lib/libmtkahypar.dylib`: +To resolve this, the attribute `com.apple.quarantine` has to be removed from the binaries inside `bin` and the dependencies inside `lib`: ``` -xattr -d com.apple.quarantine bin/ddnife -xattr -d com.apple.quarantine bin/dhone -xattr -d com.apple.quarantine lib/libmtkahypar.dylib +xattr -d com.apple.quarantine bin/* +xattr -d com.apple.quarantine lib/* ``` ## Usage -The binaries `ddnnife` and `dhone` are inside `bin`. -The Mt-KaHyPar library has to be available for `ddnnife` to run. -This can either be accomplished by moving the `lib` directories contents to the global library path (such as `/usr/lib`) -or by setting the `DYLD_LIBRARY_PATH` environment variable to include the `lib` directory. -Then, the linker will be able to find `libmtkahypar.dylib` required by `ddnife`. - +The binaries `ddnife` and `dhone` are inside `bin`. To show the help message, use: ``` diff --git a/doc/x86_64-darwin.md b/doc/x86_64-darwin.md new file mode 120000 index 0000000..e104b9b --- /dev/null +++ b/doc/x86_64-darwin.md @@ -0,0 +1 @@ +x86_64-linux.md \ No newline at end of file diff --git a/doc/built/linux-d4.md b/doc/x86_64-linux-d4.md similarity index 58% rename from doc/built/linux-d4.md rename to doc/x86_64-linux-d4.md index 76a0e29..05d0d86 100644 --- a/doc/built/linux-d4.md +++ b/doc/x86_64-linux-d4.md @@ -5,23 +5,18 @@ The project is licensed under the LGPL-3.0 and the source can be found at https: ## Dependencies -The Mt-KaHyPar dependency is bundled with this build, other dependencies have to be installed: - -- TBB (https://github.com/oneapi-src/oneTBB) -- hwloc (https://open-mpi.org/projects/hwloc) - -## Usage - -The binaries `ddnnife` and `dhone` are inside `bin`. -The Mt-KaHyPar library has to be available for `ddnnife` to run. +All dependencies are bundled with this build inside the `lib` directory. +To use the binaries, they have to be visible to the linker. This can either be accomplished by moving the `lib` directories contents to the global library path (such as `/usr/lib`) or by setting the `LD_LIBRARY_PATH` environment variable to include the `lib` directory. -Then, the linker will be able to find `libmtkahypar.so` required by `ddnnife`. +## Usage + +The binaries `ddnife` and `dhone` are inside `bin`. To show the help message, use: ``` -ddnnife --help +ddnife --help ``` For full usage instructions, see the README at https://github.com/SoftVarE-Group/d-dnnf-reasoner diff --git a/doc/built/linux.md b/doc/x86_64-linux.md similarity index 100% rename from doc/built/linux.md rename to doc/x86_64-linux.md diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..ee6d90f --- /dev/null +++ b/flake.lock @@ -0,0 +1,130 @@ +{ + "nodes": { + "crane": { + "inputs": { + "nixpkgs": [ + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1710886643, + "narHash": "sha256-saTZuv9YeZ9COHPuj8oedGdUwJZcbQ3vyRqe7NVJMsQ=", + "owner": "ipetkov", + "repo": "crane", + "rev": "5bace74e9a65165c918205cf67ad3977fe79c584", + "type": "github" + }, + "original": { + "owner": "ipetkov", + "ref": "v0.16.3", + "repo": "crane", + "type": "github" + } + }, + "d4": { + "inputs": { + "flake-utils": [ + "flake-utils" + ], + "nixpkgs": [ + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1714776063, + "narHash": "sha256-iS0m1Vv3nnbSowd92wTyhVPXzJeW/Z8PMgXVRXcXB58=", + "owner": "SoftVarE-Group", + "repo": "d4v2", + "rev": "3e12289891537485824919d5f62d57bc009d509f", + "type": "github" + }, + "original": { + "owner": "SoftVarE-Group", + "ref": "mt-kahypar", + "repo": "d4v2", + "type": "github" + } + }, + "fenix": { + "inputs": { + "nixpkgs": [ + "nixpkgs" + ], + "rust-analyzer-src": "rust-analyzer-src" + }, + "locked": { + "lastModified": 1714631076, + "narHash": "sha256-at4+1R9gx3CGvX0ZJo9GwDZyt3RzOft7qDCTsYHjI4M=", + "owner": "nix-community", + "repo": "fenix", + "rev": "22a9eb3f20dd340d084cee4426f386a90b1351ca", + "type": "github" + }, + "original": { + "owner": "nix-community", + "repo": "fenix", + "type": "github" + } + }, + "flake-utils": { + "locked": { + "lastModified": 1652776076, + "narHash": "sha256-gzTw/v1vj4dOVbpBSJX4J0DwUR6LIyXo7/SuuTJp1kM=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "04c1b180862888302ddfb2e3ad9eaa63afc60cf8", + "type": "github" + }, + "original": { + "owner": "numtide", + "ref": "v1.0.0", + "repo": "flake-utils", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1714531828, + "narHash": "sha256-ILsf3bdY/hNNI/Hu5bSt2/KbmHaAVhBbNUOdGztTHEg=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "0638fe2715d998fa81d173aad264eb671ce2ebc1", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-23.11", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "crane": "crane", + "d4": "d4", + "fenix": "fenix", + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs" + } + }, + "rust-analyzer-src": { + "flake": false, + "locked": { + "lastModified": 1714572655, + "narHash": "sha256-xjD8vmit0Nz1qaSSSpeXOK3saSvAZtOGHS2SHZE75Ek=", + "owner": "rust-lang", + "repo": "rust-analyzer", + "rev": "cfce2bb46da62950a8b70ddb0b2a12332da1b1e1", + "type": "github" + }, + "original": { + "owner": "rust-lang", + "ref": "nightly", + "repo": "rust-analyzer", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..eac06c0 --- /dev/null +++ b/flake.nix @@ -0,0 +1,144 @@ +{ + description = "Packages and development environments for ddnnife"; + + inputs = { + nixpkgs.url = "github:NixOS/nixpkgs/nixos-23.11"; + flake-utils.url = "github:numtide/flake-utils/v1.0.0"; + crane = { + url = "github:ipetkov/crane/v0.16.3"; + inputs.nixpkgs.follows = "nixpkgs"; + }; + fenix = { + url = "github:nix-community/fenix"; + inputs.nixpkgs.follows = "nixpkgs"; + }; + d4 = { + url = "github:SoftVarE-Group/d4v2/mt-kahypar"; + inputs.nixpkgs.follows = "nixpkgs"; + inputs.flake-utils.follows = "flake-utils"; + }; + }; + + outputs = { self, nixpkgs, flake-utils, crane, fenix, d4, ... }: + let + lib = nixpkgs.lib; + systems = lib.systems.doubles.unix; + in flake-utils.lib.eachDefaultSystem (system: + let + pkgs = import nixpkgs { inherit system; }; + + toolchain = fenix.packages.${system}.stable.defaultToolchain; + craneLib = (crane.mkLib pkgs).overrideToolchain toolchain; + + src = craneLib.cleanCargoSource (craneLib.path ./.); + + crateArgs = { + inherit src; + strictDeps = true; + + buildInputs = lib.optionals pkgs.stdenv.isDarwin [ pkgs.libiconv ]; + + nativeBuildInputs = [ pkgs.gnum4 ]; + + meta = with lib; { + description = "A d-DNNF reasoner"; + homepage = "https://github.com/SoftVarE-Group/d-dnnf-reasoner"; + license = licenses.lgpl3Plus; + platforms = systems; + }; + }; + + crateArgs-d4 = crateArgs // { + cargoExtraArgs = "--features d4"; + + buildInputs = + [ pkgs.boost.dev pkgs.gmp.dev d4.packages.${system}.mt-kahypar ] + ++ lib.optionals pkgs.stdenv.isDarwin [ pkgs.libiconv ]; + + nativeBuildInputs = [ pkgs.gnum4 pkgs.pkg-config ]; + + # FIXME: libcxx symbols missing (https://github.com/NixOS/nixpkgs/issues/166205) + # Should be fixed in 24.05. + env = lib.optionalAttrs pkgs.stdenv.cc.isClang { + NIX_LDFLAGS = "-l${pkgs.stdenv.cc.libcxx.cxxabi.libName}"; + }; + }; + + cargoArtifacts = craneLib.buildDepsOnly crateArgs; + cargoArtifacts-d4 = craneLib.buildDepsOnly crateArgs-d4; + in { + formatter = pkgs.nixfmt; + + checks = { + lint = craneLib.cargoClippy + (crateArgs-d4 // { cargoArtifacts = cargoArtifacts-d4; }); + + format = craneLib.cargoFmt { inherit src; }; + }; + + packages = { + default = self.packages.${system}.ddnnife-d4; + + ddnnife = craneLib.buildPackage (crateArgs // { + inherit cargoArtifacts; + doCheck = false; + }); + + ddnnife-d4 = craneLib.buildPackage (crateArgs-d4 // { + cargoArtifacts = cargoArtifacts-d4; + doCheck = false; + }); + + container = pkgs.dockerTools.buildLayeredImage { + name = "ddnnife"; + contents = [ self.packages.${system}.ddnnife-d4 ]; + config = { + Entrypoint = [ "/bin/ddnnife" ]; + Labels = { + "org.opencontainers.image.source" = + "https://github.com/SoftVarE-Group/d-dnnf-reasoner"; + "org.opencontainers.image.description" = "A d-DNNF reasoner"; + "org.opencontainers.image.licenses" = "LGPL-3.0-or-later"; + }; + }; + }; + + bundled-doc = pkgs.stdenv.mkDerivation { + name = "bundled-doc"; + src = ./doc; + installPhase = '' + mkdir $out + cp ${system}.md $out/README.md + ''; + }; + + bundled-doc-d4 = pkgs.stdenv.mkDerivation { + name = "bundled-doc-d4"; + src = ./doc; + installPhase = '' + mkdir $out + cp ${system}-d4.md $out/README.md + ''; + }; + + bundled = pkgs.buildEnv { + name = "bundled"; + paths = [ + self.packages.${system}.ddnnife + self.packages.${system}.bundled-doc + ] ++ lib.optionals pkgs.stdenv.isDarwin [ pkgs.libiconv ]; + }; + + bundled-d4 = pkgs.buildEnv { + name = "bundled-d4"; + paths = [ + self.packages.${system}.ddnnife-d4 + self.packages.${system}.bundled-doc-d4 + d4.packages.${system}.bundled-deps + ] ++ lib.optionals pkgs.stdenv.isDarwin [ pkgs.libiconv ]; + }; + }; + + devShells.default = craneLib.devShell { }; + }); +}