Stream: Coq users

Topic: Bug in Tactician


view this post on Zulip Huỳnh Trần Khanh (Apr 10 2024 at 12:30):

I'm pretty sure it must be some sort of regression. When using synth or Suggest it doesn't show suggestions on the right panel. This bug is present on coq-lsp as well as on the online demo.

When I'm less lazy I might file a GitHub issue. I currently have other stuff I gotta work on.

view this post on Zulip Ali Caglayan (Apr 10 2024 at 13:31):

Seems to work for me:
image.png

view this post on Zulip Huỳnh Trần Khanh (Apr 10 2024 at 13:49):

Screenshot_2024-04-10-20-48-38-285_com.android.chrome.jpg

view this post on Zulip Huỳnh Trần Khanh (Apr 10 2024 at 13:50):

well it's a regression it used to work fine

view this post on Zulip Huỳnh Trần Khanh (Apr 10 2024 at 13:52):

your browser might've cached an older version of the dependencies

view this post on Zulip Théo Winterhalter (Apr 10 2024 at 13:54):

I just tested the demo, having never tried it before, and it works. But the cursors has to be before the . not after like on your screenshot (I was confused at first).


Last updated: Jun 22 2024 at 16:02 UTC