add guard for HOL for now until support makes it to mainline

vprover / vampire

The Vampire Theorem Prover

https://vprover.github.io/

Other

295 stars 51 forks source link

add guard for HOL for now until support makes it to mainline #531

Closed MichaelRawson closed 8 months ago

MichaelRawson commented 8 months ago

As widely requested, until HOL support makes it into mainline we should reject HOL problems before starting any work.

The precise point of intervention is up for debate. I chose "after the problem is loaded but before preprocessing" because it's arguably simplest for a temporary fix, and I think we at least parse the majority of HOL. We should also report SZS status Inappropriate, but as this is temporary I'm inclined not to.

quickbeam123 commented 8 months ago

Is higher-orderness already correctly recognized, just after the Problem constructor?

MichaelRawson commented 8 months ago

It seems to be in testing, but you're right - I'll check.

quickbeam123 commented 8 months ago

It's fine on my side. Let me merge and reconcile the interactive mode with this.

MichaelRawson commented 8 months ago

@hetzenmat - just FYI.