Zulip Chat Archive

Stream: triage

Topic: PR #1083: feat(tactic/vampire): interface with Vampire


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Dec 14 2020 at 17:17):

(I don't know what the story changes to, but it will be different.)

view this post on Zulip 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?


Last updated: May 09 2021 at 16:20 UTC