feat: ship cadical (#4325)
Co-authored-by: Henrik Böving <hargonix@gmail.com>
This commit is contained in:
Sebastian Ullrich
GitHub
parent
bf304769e0
commit
6d4ec153ad
7 changed files with 94 additions and 5 deletions
|
|
@ -30,6 +30,32 @@ if(NOT (DEFINED STAGE0_CMAKE_EXECUTABLE_SUFFIX))
|
|||
set(STAGE0_CMAKE_EXECUTABLE_SUFFIX "${CMAKE_EXECUTABLE_SUFFIX}")
|
||||
endif()
|
||||
|
||||
# On CI Linux, we source cadical from Nix instead; see flake.nix
|
||||
find_program(CADICAL cadical)
|
||||
if(NOT CADICAL)
|
||||
set(CADICAL_CXX c++)
|
||||
find_program(CCACHE ccache)
|
||||
if(CCACHE)
|
||||
set(CADICAL_CXX "${CCACHE} ${CADICAL_CXX}")
|
||||
endif()
|
||||
# missing stdio locking API on Windows
|
||||
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
|
||||
string(APPEND CADICAL_CXXFLAGS " -DNUNLOCKED")
|
||||
endif()
|
||||
ExternalProject_add(cadical
|
||||
PREFIX cadical
|
||||
GIT_REPOSITORY https://github.com/arminbiere/cadical
|
||||
GIT_TAG rel-1.9.5
|
||||
CONFIGURE_COMMAND ""
|
||||
# https://github.com/arminbiere/cadical/blob/master/BUILD.md#manual-build
|
||||
BUILD_COMMAND $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} CXX=${CADICAL_CXX} CXXFLAGS=${CADICAL_CXXFLAGS}
|
||||
BUILD_IN_SOURCE ON
|
||||
INSTALL_COMMAND "")
|
||||
set(CADICAL ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX} CACHE FILEPATH "path to cadical binary" FORCE)
|
||||
set(EXTRA_DEPENDS "cadical")
|
||||
endif()
|
||||
list(APPEND CL_ARGS -DCADICAL=${CADICAL})
|
||||
|
||||
ExternalProject_add(stage0
|
||||
SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
|
||||
SOURCE_SUBDIR src
|
||||
|
|
|
|||
30
LICENSES
30
LICENSES
|
|
@ -1341,3 +1341,33 @@ whether future versions of the GNU Lesser General Public License shall
|
|||
apply, that proxy's public statement of acceptance of any version is
|
||||
permanent authorization for you to choose that version for the
|
||||
Library.
|
||||
==============================================================================
|
||||
CaDiCaL is under the MIT License:
|
||||
==============================================================================
|
||||
MIT License
|
||||
|
||||
Copyright (c) 2016-2021 Armin Biere, Johannes Kepler University Linz, Austria
|
||||
Copyright (c) 2020-2021 Mathias Fleury, Johannes Kepler University Linz, Austria
|
||||
Copyright (c) 2020-2021 Nils Froleyks, Johannes Kepler University Linz, Austria
|
||||
Copyright (c) 2022-2024 Katalin Fazekas, Vienna University of Technology, Austria
|
||||
Copyright (c) 2021-2024 Armin Biere, University of Freiburg, Germany
|
||||
Copyright (c) 2021-2024 Mathias Fleury, University of Freiburg, Germany
|
||||
Copyright (c) 2023-2024 Florian Pollitt, University of Freiburg, Germany
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy
|
||||
of this software and associated documentation files (the "Software"), to deal
|
||||
in the Software without restriction, including without limitation the rights
|
||||
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
|
||||
copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all
|
||||
copies or substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
||||
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
||||
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
||||
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
||||
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
|
||||
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
|
||||
SOFTWARE.
|
||||
17
flake.lock
generated
17
flake.lock
generated
|
|
@ -34,6 +34,22 @@
|
|||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs-cadical": {
|
||||
"locked": {
|
||||
"lastModified": 1722221733,
|
||||
"narHash": "sha256-sga9SrrPb+pQJxG1ttJfMPheZvDOxApFfwXCFO0H9xw=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "12bf09802d77264e441f48e25459c10c93eada2e",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "12bf09802d77264e441f48e25459c10c93eada2e",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs-old": {
|
||||
"flake": false,
|
||||
"locked": {
|
||||
|
|
@ -55,6 +71,7 @@
|
|||
"inputs": {
|
||||
"flake-utils": "flake-utils",
|
||||
"nixpkgs": "nixpkgs",
|
||||
"nixpkgs-cadical": "nixpkgs-cadical",
|
||||
"nixpkgs-old": "nixpkgs-old"
|
||||
}
|
||||
},
|
||||
|
|
|
|||
11
flake.nix
11
flake.nix
|
|
@ -5,6 +5,8 @@
|
|||
# old nixpkgs used for portable release with older glibc (2.27)
|
||||
inputs.nixpkgs-old.url = "github:NixOS/nixpkgs/nixos-19.03";
|
||||
inputs.nixpkgs-old.flake = false;
|
||||
# for cadical 1.9.5; sync with CMakeLists.txt
|
||||
inputs.nixpkgs-cadical.url = "github:NixOS/nixpkgs/12bf09802d77264e441f48e25459c10c93eada2e";
|
||||
inputs.flake-utils.url = "github:numtide/flake-utils";
|
||||
|
||||
outputs = { self, nixpkgs, nixpkgs-old, flake-utils, ... }@inputs: flake-utils.lib.eachDefaultSystem (system:
|
||||
|
|
@ -14,6 +16,11 @@
|
|||
pkgsDist-old = import nixpkgs-old { inherit system; };
|
||||
# An old nixpkgs for creating releases with an old glibc
|
||||
pkgsDist-old-aarch = import nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
|
||||
pkgsCadical = import inputs.nixpkgs-cadical { inherit system; };
|
||||
cadical = if pkgs.stdenv.isLinux then
|
||||
# use statically-linked cadical on Linux to avoid glibc versioning troubles
|
||||
pkgsCadical.pkgsStatic.cadical.overrideAttrs { doCheck = false; }
|
||||
else pkgsCadical.cadical;
|
||||
|
||||
lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; };
|
||||
|
||||
|
|
@ -21,11 +28,9 @@
|
|||
stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
|
||||
} ({
|
||||
buildInputs = with pkgs; [
|
||||
cmake gmp libuv ccache
|
||||
cmake gmp libuv ccache cadical
|
||||
lean-packages.llvmPackages.llvm # llvm-symbolizer for asan/lsan
|
||||
gdb
|
||||
# TODO: only add when proven to not affect the flakification
|
||||
#pkgs.python3
|
||||
tree # for CI
|
||||
];
|
||||
# https://github.com/NixOS/nixpkgs/issues/60919
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
{ src, debug ? false, stage0debug ? false, extraCMakeFlags ? [],
|
||||
stdenv, lib, cmake, gmp, libuv, git, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
|
||||
stdenv, lib, cmake, gmp, libuv, cadical, git, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
|
||||
... } @ args:
|
||||
with builtins;
|
||||
lib.warn "The Nix-based build is deprecated" rec {
|
||||
|
|
@ -17,7 +17,7 @@ lib.warn "The Nix-based build is deprecated" rec {
|
|||
'';
|
||||
} // args // {
|
||||
src = args.realSrc or (sourceByRegex args.src [ "[a-z].*" "CMakeLists\.txt" ]);
|
||||
cmakeFlags = (args.cmakeFlags or [ "-DSTAGE=1" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" ]) ++ (args.extraCMakeFlags or extraCMakeFlags) ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ];
|
||||
cmakeFlags = (args.cmakeFlags or [ "-DSTAGE=1" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" "-DCADICAL=${cadical}/bin/cadical" ]) ++ (args.extraCMakeFlags or extraCMakeFlags) ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ];
|
||||
preConfigure = args.preConfigure or "" + ''
|
||||
# ignore absence of submodule
|
||||
sed -i 's!lake/Lake.lean!!' CMakeLists.txt
|
||||
|
|
|
|||
|
|
@ -633,6 +633,10 @@ file(COPY ${LEAN_SOURCE_DIR}/bin/leanmake DESTINATION ${CMAKE_BINARY_DIR}/bin)
|
|||
|
||||
install(DIRECTORY "${CMAKE_BINARY_DIR}/bin/" USE_SOURCE_PERMISSIONS DESTINATION bin)
|
||||
|
||||
if (${STAGE} GREATER 0)
|
||||
install(PROGRAMS "${CADICAL}" DESTINATION bin)
|
||||
endif()
|
||||
|
||||
add_custom_target(clean-stdlib
|
||||
COMMAND rm -rf "${CMAKE_BINARY_DIR}/lib" || true)
|
||||
|
||||
|
|
|
|||
7
src/cadical.mk
Normal file
7
src/cadical.mk
Normal file
|
|
@ -0,0 +1,7 @@
|
|||
CXX ?= c++
|
||||
|
||||
%.o: src/%.cpp
|
||||
$(CXX) -std=c++11 -O3 -DNDEBUG -DNBUILD $(CXXFLAGS) -c $< -o $@
|
||||
|
||||
../../cadical$(CMAKE_EXECUTABLE_SUFFIX): $(patsubst src/%.cpp,%.o,$(shell ls src/*.cpp | grep -v mobical))
|
||||
$(CXX) -o $@ $^
|
||||
Loading…
Add table
Reference in a new issue