Stream: General

Topic: Possible leak of CNF files during Sledgehammer invocations

Yutaka Nagashima (Jun 23 2026 at 10:14):

Hello,

While running a large-scale evaluation using Isabelle2025-2 on Ubuntu 22.04, I observed a substantial accumulation of temporary files with names of the form

/tmp/tmpXXXXXXXXXXXXXXXcnf

during repeated automated proof attempts involving Sledgehammer.

In one run, approximately 10,000 such files accumulated and occupied about 10 GB of disk space:

I have not yet identified which component is responsible for creating these files, nor whether their persistence is intentional.

Before investigating further, I would like to ask:

1. Is the creation and retention of these .cnf files expected behaviour?
2. Which Isabelle component (or external prover) is responsible for them?
3. Is there a documented mechanism for cleaning them up automatically?

If the current behaviour is intentional, it might nevertheless be helpful to document it, as heavy users may otherwise be surprised by the amount of disk space consumed over time.

I would be happy to provide additional details or a reproducer if useful.

Best regards,
Yutaka

Mathias Fleury (Jun 23 2026 at 18:31):

Never seen any .cnf file when running sledgehammer

Mathias Fleury (Jun 23 2026 at 18:32):

The only culprint I could assume is that sat (https://isabelle.in.tum.de/library/HOL/HOL-Proofs/ISABELLE_HOME/src/HOL/Tools/sat_solver.ML.html) is producing some files, but:

- I am not aware that sledgehammer even runs sat
- those file have a header on the first line

Fabian Huch (Jun 24 2026 at 07:28):

Since these are not Isabelle temp files, this must be some external tool

Mathias Fleury (Jun 24 2026 at 09:47):

Some tools have options to write intermediate files

Mathias Fleury (Jun 24 2026 at 09:47):

(sledgehammer has for example, but you have to set the options)

Lawrence Paulson (Jun 28 2026 at 21:32):

Looks like you have minisat_with_proofs as one of your solvers. I wasn't aware of its existence, but it writes those files. Did it prove anything?

Yutaka Nagashima (Jun 30 2026 at 13:32):

Thanks. I wasn't aware that minisat_with_proofs writes those files.

I don't explicitly invoke minisat_with_proofs myself. In AbductionProver/PSL, I invoke Sledgehammer via Sledgehammer.run_sledgehammer with the default parameters (apart from a couple of options such as isar_proofs=false), so if minisat_with_proofs is being used, it is through Sledgehammer's default behaviour.

As for whether it actually proved anything, I'm honestly not sure. Since AbductionProver invokes Sledgehammer many times during a single proof search, it is difficult to tell which internal components contributed to a successful proof.

For my own evaluation, I now delete these *cnf files after each run, so the immediate problem is under control. I reported this because I suspect it may also affect other users who invoke Sledgehammer repeatedly.

With the recent trend of combining Sledgehammer with external AI components and agentic proof search, repeatedly calling Sledgehammer is becoming increasingly common, so others may eventually run into the same issue.

Mathias Fleury (Jul 01 2026 at 19:52):

Thanks. I wasn't aware that minisat_with_proofs writes those files.

As Fabian said, the naming scheme just does not match those files:

    val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
    val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
    val proofpath  = File.tmp_path (Path.explode ("result" ^ serial_str ^ ".prf"))

Mathias Fleury (Jul 01 2026 at 19:53):

None of those files starts with "tmp"

Last updated: Jul 02 2026 at 14:06 UTC