How is Cadical used in Lean and Mathlib?

Stream: new members

[Isak Colboubrani]

I noticed that building Lean also builds the CaDiCaL SAT Solver:

% stage1/bin/cadical
c --- [ banner ] -------------------------------------------------------------
c
c CaDiCaL SAT Solver
c Copyright (c) 2016-2023 A. Biere, M. Fleury, N. Froleyks, K. Fazekas, F. Pollitt
c
c Version 1.9.5

How is Cadical used in Lean?

Is it used by Mathlib yet?

[Henrik Böving]

bv_decide and friends use cadical

[Isak Colboubrani]

Thanks! Those are bv_check, bv_decide, bv_normalize and bv_omega?

If so none of them seems to be used by Mathlib as of master.

[Henrik Böving]

bv_omega not

[Henrik Böving]

And that's correct, mathlib doesn't do BitVec theory after all

[Eric Wieser]

Cadical is a new dependency in 4.12.0, right?

[Eric Wieser]

Is it an optional one, or required?

[Henrik Böving]

It's not a dependency, Lean ships it on its own.

[Eric Wieser]

It's a dependency if you build from source though?

[Henrik Böving]

No, if it's not installed it will compile the thing on its own

[Isak Colboubrani]

It qualifies as a dependency in the sense that it is an external software component that the project relies on to function properly.

However, it does not qualify as a dependency in the sense that you need to have it installed before compiling Lean.

Does that sound reasonable?

[Henrik Böving]

yes that's correct