I will not respond further on this in this thread.
On Thursday, April 11, 2024 at 1:15:52 PM UTC-7 Dima Pasechnik wrote:
>
>
> On 11 April 2024 21:47:57 CEST, Matthias Koeppe
> wrote:
> >Once again, the workflow files in .github/workflows have to be statically
> >present in a repository so
On 11 April 2024 21:47:57 CEST, Matthias Koeppe
wrote:
>Once again, the workflow files in .github/workflows have to be statically
>present in a repository so that Actions work.
>And the .devcontainers files have to be statically present in a repository
>so that Codespaces work.
Yes, sure,
Once again, the workflow files in .github/workflows have to be statically
present in a repository so that Actions work.
And the .devcontainers files have to be statically present in a repository
so that Codespaces work.
If you want to propose a design for breaking our repository into multiple
On 11 April 2024 18:06:42 CEST, Matthias Koeppe
wrote:
>On Thursday, April 11, 2024 at 4:28:12 AM UTC-7 dim...@gmail.com wrote:
>
>On Wed, Apr 10, 2024 at 04:23:13PM -0700, Matthias Koeppe wrote:
>> On Wednesday, April 10, 2024 at 3:25:16 PM UTC-7 Dima Pasechnik wrote:
>> Necessary reminder
On Thursday, April 11, 2024 at 4:28:12 AM UTC-7 dim...@gmail.com wrote:
On Wed, Apr 10, 2024 at 04:23:13PM -0700, Matthias Koeppe wrote:
> On Wednesday, April 10, 2024 at 3:25:16 PM UTC-7 Dima Pasechnik wrote:
> Necessary reminder that we're discussing, as the subject says, the files
> that
On Wed, Apr 10, 2024 at 04:23:13PM -0700, Matthias Koeppe wrote:
> On Wednesday, April 10, 2024 at 3:25:16 PM UTC-7 Dima Pasechnik wrote:
>
> On Wed, Apr 10, 2024 at 11:10 PM Matthias Koeppe
> wrote:
>
> On Wednesday, April 10, 2024 at 2:40:18 PM UTC-7 Dima Pasechnik wrote:
>
> There is
On Wednesday, April 10, 2024 at 3:25:16 PM UTC-7 Dima Pasechnik wrote:
On Wed, Apr 10, 2024 at 11:10 PM Matthias Koeppe
wrote:
On Wednesday, April 10, 2024 at 2:40:18 PM UTC-7 Dima Pasechnik wrote:
There is simply no need to keep the .gitsubmodules -
the only file in the main repo affected
On Wed, Apr 10, 2024 at 11:10 PM Matthias Koeppe
wrote:
> On Wednesday, April 10, 2024 at 2:40:18 PM UTC-7 Dima Pasechnik wrote:
>
> On Wed, Apr 10, 2024 at 9:02 PM Matthias Koeppe
> wrote:
>
> On Wednesday, April 10, 2024 at 1:00:06 PM UTC-7 Dima Pasechnik wrote:
>
> On 10 April 2024 19:24:12
On Wednesday, April 10, 2024 at 2:40:18 PM UTC-7 Dima Pasechnik wrote:
On Wed, Apr 10, 2024 at 9:02 PM Matthias Koeppe
wrote:
On Wednesday, April 10, 2024 at 1:00:06 PM UTC-7 Dima Pasechnik wrote:
On 10 April 2024 19:24:12 CEST, Matthias Koeppe
wrote:
>On Tuesday, April 9, 2024 at 3:28:27
On Wed, Apr 10, 2024 at 9:02 PM Matthias Koeppe
wrote:
> On Wednesday, April 10, 2024 at 1:00:06 PM UTC-7 Dima Pasechnik wrote:
>
> On 10 April 2024 19:24:12 CEST, Matthias Koeppe
> wrote:
> >On Tuesday, April 9, 2024 at 3:28:27 PM UTC-7 Dima Pasechnik wrote:
> >
> >[...] git submodules [...]
>
On Wednesday, April 10, 2024 at 1:00:06 PM UTC-7 Dima Pasechnik wrote:
On 10 April 2024 19:24:12 CEST, Matthias Koeppe
wrote:
>On Tuesday, April 9, 2024 at 3:28:27 PM UTC-7 Dima Pasechnik wrote:
>
>[...] git submodules [...]
>
>git submodules are included in a repository by specific commit
On 10 April 2024 19:24:12 CEST, Matthias Koeppe
wrote:
>On Tuesday, April 9, 2024 at 3:28:27 PM UTC-7 Dima Pasechnik wrote:
>
>[...] git submodules [...]
>
>
>git submodules are included in a repository by specific commit sha of the
>submodule repo.
>So whenever one has to make a change in
On Tuesday, April 9, 2024 at 6:39:00 PM UTC-7 Kwankyu Lee wrote:
How about redefining the meaning of "CI Fix" label:
1. We designate a person to be the CI manager.
2. For PRs pertaining to the designated directories and files, we add "CI
Fix" label
3. The CI manager has the right to merge PRs
On Tuesday, April 9, 2024 at 3:28:27 PM UTC-7 Dima Pasechnik wrote:
[...] git submodules [...]
git submodules are included in a repository by specific commit sha of the
submodule repo.
So whenever one has to make a change in the submodule repo, one also has to
commit a change (by a second PR)
On 10 April 2024 03:39:00 CEST, Kwankyu Lee wrote:
>How about redefining the meaning of "CI Fix" label:
>
>1. We designate a person to be the CI manager.
>2. For PRs pertaining to the designated directories and files, we add "CI
>Fix" label
>3. The CI manager has the right to merge PRs with
On 10 April 2024 02:04:48 CEST, Matthias Koeppe
wrote:
>On Tuesday, April 9, 2024 at 4:20:56 PM UTC-7 Dima Pasechnik wrote:
>
>have a CI/sage-distro repo [...] with all that .github/ etc stuff needed
>for CI, including a part of build/ - and checkout sagelib as a submodule.
>
>
>Also that
How about redefining the meaning of "CI Fix" label:
1. We designate a person to be the CI manager.
2. For PRs pertaining to the designated directories and files, we add "CI
Fix" label
3. The CI manager has the right to merge PRs with "CI Fix" label to develop.
4. The old meaning of "CI Fix"
On Tuesday, April 9, 2024 at 4:20:56 PM UTC-7 Dima Pasechnik wrote:
have a CI/sage-distro repo [...] with all that .github/ etc stuff needed
for CI, including a part of build/ - and checkout sagelib as a submodule.
Also that does not work. Part of the .github/workflows is to run the CI on
the
On 10 April 2024 00:51:33 CEST, Matthias Koeppe
wrote:
>On Tuesday, April 9, 2024 at 3:28:27 PM UTC-7 Dima Pasechnik wrote:
>
>How about moving them out of the main Sage tree into separate repos, which
>can be accessed from the main tree as git submodules?
>
>
>That does not work.
Oops. Experimenting with this idea, I accidentally pushed a "crazy" commit
to "develop". Please revoke the commit ASAP!
I *mv*ed ".github" directory to "github" and made a symlink ".github ->
github" to see if this works, in my own repo. But I accidentally pushed to
sagemath/sage!
I
On Wednesday, April 10, 2024 at 7:51:34 AM UTC+9 Matthias Koeppe wrote:
On Tuesday, April 9, 2024 at 3:28:27 PM UTC-7 Dima Pasechnik wrote:
How about moving them out of the main Sage tree into separate repos, which
can be accessed from the main tree as git submodules?
That does not work.
On Tuesday, April 9, 2024 at 3:28:27 PM UTC-7 Dima Pasechnik wrote:
How about moving them out of the main Sage tree into separate repos, which
can be accessed from the main tree as git submodules?
That does not work.
.github/workflows orchestrates what runs in the repo -- so it has to be in
On 9 April 2024 23:11:59 CEST, Matthias Koeppe wrote:
>Dear Sage developers:
>I propose to consider the following governance change for a small part of
>the Sage repository:
>1. The directories *.ci, .devcontainer, .github/workflows*. These are
>special directories that control the GitHub
Dear Sage developers:
I propose to consider the following governance change for a small part of
the Sage repository:
1. The directories *.ci, .devcontainer, .github/workflows*. These are
special directories that control the GitHub workflows that run for example
on pull requests and when release
24 matches
Mail list logo
