elisabeth lemma (Mar 13 2025 at 14:05): elisabeth lemma (Mar 13 2025 at 14:05):hi everyone,
i'm trying to use cvc5 as an smt-solver to prove things with the smt-tactic. could somebody ELI5 which cvc5 version need to download (from here: https://github.com/cvc5/cvc5/releases/tag/cvc5-1.2.1 i'm assuming? or do i need to build it myself?) and what i need to tell isabelle so that isabelle will find cvc5? i'm on linux
my code and my error message for completion's sake
Lukas Stevens (Mar 13 2025 at 14:23):Can you elaborate on what you are trying to achieve? Isabelle2024 is shipped with cvc4. Isabelle2025, which was just released, comes with cvc5.
Lukas Stevens (Mar 13 2025 at 14:23):So you might want to switch to Isabelle2025
elisabeth lemma (Mar 13 2025 at 14:27):oh :woman_facepalming: i see, thanks for the quick response. i'll figure it out
Mathias Fleury (Mar 13 2025 at 16:32):for cvc5 in the smt tactic: this is work in progress by Hanna and me (for the Isabelle side, there are more people on the cvc5 side)
Mathias Fleury (Mar 13 2025 at 16:33):(outside repo)
Mathias Fleury (Mar 13 2025 at 16:55):In Isabelle 2025, cvc5 is only used for sledgeghammer
elisabeth lemma (Mar 14 2025 at 00:55):yeah i'm currently hacking around in sledgehammer on some undetermined repo fork version, i wasn't aware that cvc5 was a WIP/new feature and misread the error message, so i just assumed i was missing something really obvious, that's why i asked here. sorry for the confusion :pray:
Last updated: Apr 18 2025 at 20:21 UTC