Closed JacquesCarette closed 4 weeks ago
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₁
.
Will do a little later today.
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
⊥-elim
tocontradiction
everywhere 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.
I've now allowed edits. Sorry about that.
Summary of routine changes:
.Base
for many modules instead of the "fat" top-level modulesFunction
(Function.Equivalence
, etc) and replace withFunction.Bundles
¬_
fromRelation.Unary.Negation
Relation.Nullary.Decidable
where they now liveMust-be-done changes that may need a bit more text:
_≡⟨⟩_
is now syntax, so need to importstep-≡-∣
insteadstep-≡
is nowstep-≡-⟩
data List′ : Set → Set where
is 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:
contradiction
instead of⊥-elim