Skip to content

Added user script in coqbot.sh for doside in coq/coq #1577

Added user script in coqbot.sh for doside in coq/coq

Added user script in coqbot.sh for doside in coq/coq #1577

Triggered via push October 9, 2023 09:26
Status Success
Total duration 2m 5s
Artifacts 7

main.yml

on: push
Fit to window
Zoom out
Zoom in

Annotations

1 error and 1 warning
build: thebug.v#L3
Syntax Error: Lexer: Undefined token
build
Running command /usr/bin/python3 /github/workspace/coq-tools/find-bug.py -y /github/workspace/thebug.v /github/workspace/cwd/bug_01.v /github/workspace/cwd/tmp.v --error-log=/github/workspace/build.log --no-deps --ignore-coq-prog-args --inline-user-contrib --coqc=/home/coq/.opam/4.13.1+flambda/bin/coqc.orig --coqtop=/home/coq/.opam/4.13.1+flambda/bin/coqtop.orig --coq_makefile=/home/coq/.opam/4.13.1+flambda/bin/coq_makefile --coqdep /home/coq/.opam/4.13.1+flambda/bin/coqdep --base-dir=/github/workspace/builds/coq/coq-failing/_build_ci/ -Q /github/workspace/cwd Top --verbose-include-failure-warning --verbose-include-failure-warning-prefix ::warning:: --verbose-include-failure-warning-newline --arg=-q -l - /github/workspace/bug.log --verbose-log-file 9999\,/github/workspace/bug.verbose.log

Artifacts

Produced during runtime
Name Size
artifact Expired
1.3 MB
bug.log Expired
67.2 KB
bug.v Expired
666 Bytes
bug.verbose.log Expired
1000 KB
build.log Expired
14.7 KB
metadata Expired
154 Bytes
tmp.v Expired
0 Bytes