hacspec
Phase setup hard to use
The errors for misalignment between phases and/or features results in an error, printing a comparison between the two module definitions. This is hard to read, and figuring out what is required to fix it is not intuitive. We should either improve the error messages, to explain exactly what is wrong, without too much filler text; or have a description of which phases are required for each phase you want to add, and what features the combination results in.
Yes, when OCaml cannot unify two module signatures, the error it prints is very very verbose and hard to read...
We want to have more docs on those, see https://github.com/cryspen/hax/issues/1141. We also would like to have a runtime system for invariants, see https://github.com/cryspen/hax/issues/939. And better tooling for adding a phase, see https://github.com/cryspen/hax/issues/1032. Being able to infer the list of features required at a given point would be great, too.
This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.
![github-actions[bot] avatar](https://avatars.githubusercontent.com/in/15368?v=4 "Published by a pub.dev verified publisher"){kind=small}
We are re-architecting this part, and so we won't address this for now.
This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.
Closing this as unplanned. The ergonomics should be better in the Rust engine.
