Zulip Chat Archive
Stream: triage
Topic: PR #1083: feat(tactic/vampire): interface with Vampire
Random Issue Bot (Dec 14 2020 at 14:25):
Today I chose PR 1083 for discussion!
feat(tactic/vampire): interface with Vampire
Created by @None (@skbaek) on 2019-05-25
Labels: WIP, merge-conflict, please-adopt
Is this PR still relevant? Any recent updates? Anyone making progress?
Rob Lewis (Dec 14 2020 at 15:49):
This is not going to be merged, it's really just proof of concept. Since people occasionally ask about this kind of thing it's worth keeping the PR open for visibility.
Mario Carneiro (Dec 14 2020 at 17:11):
Is there a path forward for tools like this, if not exactly this implementation? What would it look like?
Rob Lewis (Dec 14 2020 at 17:16):
I think the story changes substantially with Lean 4, so it might not be worth tracing the path for Lean 3.
Rob Lewis (Dec 14 2020 at 17:17):
(I don't know what the story changes to, but it will be different.)
Random Issue Bot (Mar 30 2021 at 14:23):
Today I chose PR 1083 for discussion!
feat(tactic/vampire): interface with Vampire
Created by @None (@skbaek) on 2019-05-25
Labels: WIP, merge-conflict, please-adopt
Is this PR still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jun 03 2022 at 14:18):
Today I chose PR 1083 for discussion!
feat(tactic/vampire): interface with Vampire
Created by @None (@skbaek) on 2019-05-25
Labels: WIP, please-adopt, merge-conflict
Is this PR still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC