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

Make print-pretty-timed robust against non-output-sync logs #13063

Merged
merged 1 commit into from
Sep 22, 2020
Merged

Make print-pretty-timed robust against non-output-sync logs #13063

merged 1 commit into from
Sep 22, 2020

Conversation

JasonGross
Copy link
Member

Also pass --output-sync on the CI, as suggested in
#12653 (comment), to protect
against this failure mode.

Kind: bug fix / infrastructure.

Fixes / closes #13062

@JasonGross
Make print-pretty-timed robust against non-output-sync logs
fef5b75 
Also pass `--output-sync` on the CI, as suggested in
coq#12653 (comment), to protect
against this failure mode.

Fixes coq#13062
@JasonGross JasonGross added kind: fix This fixes a bug or incorrect documentation. kind: infrastructure CI, build tools, development tools. part: tools Coqdoc, coq_makefile, etc. labels Sep 21, 2020
@JasonGross JasonGross added this to the 8.12.1 milestone Sep 21, 2020
@JasonGross JasonGross requested review from a team as code owners September 21, 2020 16:43
@JasonGross JasonGross mentioned this pull request Sep 21, 2020
Merged
JasonGross added a commit to JasonGross/coq-scripts that referenced this pull request Sep 21, 2020
@JasonGross
Make timing script robust against interleaving
9464ceb 
See also coq/coq#13063
@SkySkimmer SkySkimmer self-assigned this Sep 22, 2020
@SkySkimmer
Copy link
Contributor

@coqbot: merge now

@coqbot-app coqbot-app bot merged commit 16813b5 into coq:master Sep 22, 2020
Zimmi48 added a commit to Zimmi48/coq that referenced this pull request Sep 22, 2020
@Zimmi48
Backport PR coq#13063: Make print-pretty-timed robust against non-out…
99f7cf5 
…put-sync logs
@JasonGross JasonGross deleted the fix-no-output-sync-make-file branch September 22, 2020 20:51
Zimmi48 added a commit to Zimmi48/coq that referenced this pull request Sep 23, 2020
@Zimmi48
Backport PR coq#13063: Make print-pretty-timed robust against non-out…
809fd50 
…put-sync logs
@SkySkimmer
Copy link
Contributor

output-sync seems to change make output in a bad way: the Leaving directory ... line gets printed before the output of the commands run in that directory. This confuses emacs such that it can't jump to error locations.

@Zimmi48
Copy link
Member

Zimmi48 commented Oct 16, 2020

Not a big deal for 8.12.1, right? I just want to verify that I shouldn't revert this PR in v8.12.

@SkySkimmer SkySkimmer mentioned this pull request Mar 29, 2021
Merged
@JasonGross
Copy link
Member Author

We could pass --no-print-directory if we want to disable it, though I seem to recall there being some objection to this...

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels
kind: fix This fixes a bug or incorrect documentation. kind: infrastructure CI, build tools, development tools. part: tools Coqdoc, coq_makefile, etc.
Projects
None yet
Milestone
8.12.1
Development

Successfully merging this pull request may close these issues.

make print-pretty-timed can fail in rare cases without --output-sync
3 participants
@JasonGross @SkySkimmer @Zimmi48