search

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.41k stars 339 forks source link

Remove fiddly attempt at instance postponement #7298

Closed plt-amy closed 3 weeks ago

plt-amy commented 3 weeks ago

Fixes #7295. The deleted code was just an attempt at reducing the amount of instance candidates we'd consider before necessary; it turns out not to have too great an effect to begin with, in addition to being extra fiddly, so I'm just going to get rid of it. In addition to the issues with scheduling constraints, it violates the invariant that instance selection should not depend on the discrimination tree returning a minimal set of constraints.

andreasabel commented 3 weeks ago

Seems to be a (hopefully temporary) problem with GitHub actions:

plt-amy commented 3 weeks ago

Yeah, actions were randomly being skipped in the 1Lab repo too.. I tried to kick them into starting last night, but I guess I'll just do the time-honored approach of pushing a whitespace change to get a CI run. Fwiw, succeed, fail and interaction all passed locally

andreasabel commented 3 weeks ago

Closing and reopening a PR also restarts the checks.

plt-amy commented 3 weeks ago

@andreasabel Nice, thank you! Scary notification to wake up to but I guess GitHub servers have sorted themselves out