plfa
Port PLFA to work with agda-2.7 and stdlib-2.1
Summary of routine changes:
- use
.Basefor many modules instead of the "fat" top-level modules - don't use any deprecated modules under
Function(Function.Equivalence, etc) and replace withFunction.Bundles - get
¬_fromRelation.Unary.Negation - get all the decidable predicates from
Relation.Nullary.Decidablewhere they now live - partial clean up of useless imports
Must-be-done changes that may need a bit more text:
-
_≡⟨⟩_is now syntax, so need to importstep-≡-∣instead -
step-≡is nowstep-≡-⟩ -
data List′ : Set → Set whereis no longer equivalent toList(and doesn't even typecheck anymore with an option to allow large eliminations). I replaced the codomain withSet₁and added a short sentence about it. I would actually recommend deletingList'entirely as the "better" change.
Stylistic changes to fit the 2.1 style better:
- in a couple of places, use
contradictioninstead of⊥-elim
Predictably, the build failed. My skills at CI may not be up to changing the scripts to fix that. Help?
Thanks very much for doing this, Jacques!
I will ask Wen to look at fixing the CI. She is submitting her PhD dissertation just now, so it may take a while.
Following are suggested changes to your pull request. Can you modify to include these?
Induction, line 31, should be:
(Importing step-≡-I defines _≡⟨⟩_ and importing step-≡-⟩ defines _≡⟨_⟩_.)
Lists, lines 68-69, should be:
This is almost equivalent, save that with parameterised types the result can be Set,
whereas for technical reasons indexed types require the result type to be Set₁.
Thanks! I've written to Wen to ask when she can update the CI. When does your term begin? (Edinburgh begins week 3 of September.)
Oops, I see Induction, line 24, also needs to change:
Old: cong, sym, and _≡⟨_⟩_, which are explained below:
New: cong, sym, _≡⟨⟩_ and _≡⟨_⟩_, which are explained below:
Also, a couple of background questions:
Was your intention to change ⊥-elim to contradiction everywhere it appears? I think I spotted some places where ⊥-elim was left unchanged.
Where can I read up on the change that leads to most imports ending .Base?
@JacquesCarette did you update the git submodule for the standard library? There's a bunch of Agda errors on CI that make me believe it's still using the older version.
When does your term begin?
Next Tuesday, September 3rd.
Was your intention to change
⊥-elimtocontradictioneverywhere it appears?
Probably not everywhere: it makes sense in part 1 to define it as it is. But, in practice, contradiction tends to make it clearer to the reader what is going on. I can certainly be more systematic if that is desired.
Where can I read up on the change that leads to most imports ending .Base?
There is, as of yet, no single place. There is a lot of conversation in stdlib issues and PRs related to that.
The design of the library (since 2.0) is to put the most basic definitions for X in Data.X.Base, the properties of X in Data.X.Properties and then have a "batteries included" module Data.X. So Data.X tends to be a convenient import when just getting work done, and then one tends to clean up afterwards for more precision and faster loading speed.
@wenkokke I neither updated the git submodule for the standard library nor the version of Agda in this PR. Obviously, I did do that in my working environment, but not through a git submodule for stdlib but rather through Agda's own library management features.
My git & CI powers are currently insufficient to be confident in making those changes correctly.
Also, a couple of background questions:
Where can I read up on the change that leads to most imports ending .Base?
Presumably, the changelog for agda stdlib.
This is likely a continuation of the trend towards more lightweight modules, so it's not essential, but probably shaves some time off the checking.
@wenkokke I neither updated the git submodule for the standard library nor the version of Agda in this PR. Obviously, I did do that in my working environment, but not through a git submodule for stdlib but rather through Agda's own library management features.
My git & CI powers are currently insufficient to be confident in making those changes correctly.
I'll add an entry to CONTRIBUTING.md while I do it.
Closing this in favour of #1028.
(@JacquesCarette you disallowed maintainers pushing to your branch, so I've made my own copy of your branch.)
That was a mistake - I wanted the exact opposite, i.e. allow maintainers to push! I could fix it... I would want the 'credit' of doing official, accepted PRs on here.