Stream: Coq devs & plugin devs

Topic: ✔ Add LoadPath vs Add Rec Loadpath


view this post on Zulip Arpan Agrawal (Jan 02 2024 at 21:03):

Got it, thanks!

view this post on Zulip Notification Bot (Jan 02 2024 at 21:03):

Arpan Agrawal has marked this topic as resolved.

view this post on Zulip Arpan Agrawal (Jan 09 2024 at 20:44):

@Gaëtan Gilbert, I'm still running into issues with this, and I'm getting different error messages on two different opam switches (both using Coq 8.12). This is my _CoqProject file: https://github.com/agrarpan/pumpkin-pi/blob/coq-8.12/plugin/_CoqProject

When I run coqc coq/TestLift.v, I get either "Test not found" or "ornaments.cxms" not found. Could you please tell me what I'm doing wrong?


Last updated: Oct 13 2024 at 01:02 UTC