-
-
Save JasonGross/3f9aa67a376c84732bc268ea4da86031 to your computer and use it in GitHub Desktop.
coq-bench config
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Skip to content | |
| titletitle jgross@mit.edu | log out | |
| search | |
| Jenkins | |
| opam | |
| benchmark-part-of-the-branch | |
| configuration | |
| Back to Dashboard | |
| Status | |
| Changes | |
| Workspace | |
| Build with Parameters | |
| Delete Project | |
| Configure | |
| Rebuild Last | |
| collapsetrend60%Build History | |
| x | |
| find | |
| Success > Console OutputTrigger CS from Pretyping: #12383, coq-engine-bench x4 | |
| May 28, 2020 11:12 AM | |
| Feel free to kill this if it's taking too long and you need to bench something else! | |
| Failed > Console OutputParametric rings | |
| May 25, 2020 11:47 PM | |
| Failed > Console Outputbroken config | |
| May 25, 2020 11:30 PM | |
| unclear why | |
| Success > Console Outputwork on eauto | |
| May 25, 2020 8:09 AM | |
| Success > Console OutputTrigger CS from Pretyping: #12383 | |
| May 22, 2020 3:08 PM | |
| https://github.com/coq/coq/pull/12383 | |
| Success > Console Outputwork on eauto | |
| May 20, 2020 3:53 PM | |
| Success > Console OutputCS allowed on dependent function space | |
| May 19, 2020 4:02 PM | |
| Success > Console OutputRemove redundant data from VM case switch. | |
| May 17, 2020 2:15 PM | |
| Success > Console Output[misc] Better preserve backtraces in several modules | |
| May 15, 2020 1:35 PM | |
| Success > Console Output[exn] [tactics] improve backtraces on monadic errors | |
| May 14, 2020 9:37 PM | |
| Aborted > Console Output[misc] Better preserve backtraces in several modules | |
| May 14, 2020 9:29 PM | |
| Success > Console Outputcclosure: lookup const bodies in a map without opaques | |
| May 10, 2020 12:08 PM | |
| Success > Console OutputHack a prototype on-disk offloading similar to ocaml-ancient. | |
| May 9, 2020 2:30 PM | |
| Success > Console OutputDeclare more Permutation instances as Global | |
| May 8, 2020 12:00 AM | |
| Failed > Console Outputeauto cleanup | |
| May 7, 2020 11:32 AM | |
| Success > Console Outputssr cleanups | |
| May 5, 2020 9:02 AM | |
| Success > Console OutputTest relevance before structural equality for constants | |
| May 4, 2020 2:50 PM | |
| just unimath | |
| Success > Console OutputV82 API ports | |
| May 3, 2020 1:11 PM | |
| Success > Console OutputLocating error again in TacAtom and TacAlias | |
| May 2, 2020 2:42 PM | |
| Failed > Console OutputTest locating tactic errors (PR #12223) | |
| May 1, 2020 9:51 PM | |
| Success > Console OutputTest relevance before structural equality for rels and constants | |
| Apr 30, 2020 10:07 PM | |
| Success > Console OutputLtacProf now handles multi-success backtracking | |
| Apr 30, 2020 4:16 AM | |
| Failed > Console OutputTest relevance before structural equality for rels and constants | |
| Apr 29, 2020 2:39 PM | |
| Success > Console OutputLtacProf now handles multi-success backtracking | |
| Apr 28, 2020 10:42 PM | |
| Success > Console OutputDo not delay the loading of the library_disk field when requiring libraries. | |
| Apr 27, 2020 5:28 PM | |
| Success > Console OutputTry not hashconsing private constants. | |
| Apr 26, 2020 11:41 PM | |
| Failed > Console OutputStop relying on side-effects for recursive scheme declaration. | |
| Apr 25, 2020 1:05 PM | |
| Failed > Console Output[exn] [tactics] improve backtraces on monadic errors | |
| Apr 23, 2020 4:31 AM | |
| flambda both sides | |
| Failed > Console Output[exn] [tactics] improve backtraces on monadic errors | |
| Apr 22, 2020 2:14 PM | |
| Failed > Console Outputv8.11 vs master [again] | |
| Apr 14, 2020 5:39 AM | |
| Jason has been reporting some strange failures, let's see if memory use has gone wrong in some way | |
| Feed RSS for all Feed RSS for failures | |
| Project name | |
| benchmark-part-of-the-branch | |
| Description | |
| [Safe HTML] Preview | |
| This build is parameterized Help for feature: This build is parameterized | |
| String Parameter | |
| [Help] | |
| Name | |
| new_coq_repository | |
| Help for feature: Name | |
| Default Value | |
| Help for feature: Default Value | |
| Description | |
| The repository which holds the "new commit". | |
| [Safe HTML] Preview Help for feature: Description | |
| Delete | |
| String Parameter | |
| [Help] | |
| Name | |
| new_coq_commit | |
| Help for feature: Name | |
| Default Value | |
| Help for feature: Default Value | |
| Description | |
| The commit designating the branch that holds the changes you want to benchmark. | |
| Must be the full hash (no branch or short hash) | |
| [Safe HTML] Preview Help for feature: Description | |
| Delete | |
| String Parameter | |
| [Help] | |
| Name | |
| new_coq_opam_archive_git_uri | |
| Help for feature: Name | |
| Default Value | |
| https://github.com/coq/opam-coq-archive.git | |
| Help for feature: Default Value | |
| Description | |
| You can change this value if you want to use customized OPAM packages with <code>new_coq_commit</code>. | |
| [Safe HTML] Preview Help for feature: Description | |
| Delete | |
| String Parameter | |
| [Help] | |
| Name | |
| new_coq_opam_archive_git_branch | |
| Help for feature: Name | |
| Default Value | |
| master | |
| Help for feature: Default Value | |
| Description | |
| [Safe HTML] Preview Help for feature: Description | |
| Delete | |
| String Parameter | |
| [Help] | |
| Name | |
| old_coq_repository | |
| Help for feature: Name | |
| Default Value | |
| https://github.com/coq/coq.git | |
| Help for feature: Default Value | |
| Description | |
| The repository that contains the referential commit (against which you want to compare your changes). | |
| [Safe HTML] Preview Help for feature: Description | |
| Delete | |
| String Parameter | |
| [Help] | |
| Name | |
| old_coq_commit | |
| Help for feature: Name | |
| Default Value | |
| Help for feature: Default Value | |
| Description | |
| The referential commit (against which you want to compare your changes). | |
| [Safe HTML] Preview Help for feature: Description | |
| Delete | |
| String Parameter | |
| [Help] | |
| Name | |
| old_coq_opam_archive_git_uri | |
| Help for feature: Name | |
| Default Value | |
| https://github.com/coq/opam-coq-archive.git | |
| Help for feature: Default Value | |
| Description | |
| [Safe HTML] Preview Help for feature: Description | |
| Delete | |
| String Parameter | |
| [Help] | |
| Name | |
| old_coq_opam_archive_git_branch | |
| Help for feature: Name | |
| Default Value | |
| master | |
| Help for feature: Default Value | |
| Description | |
| [Safe HTML] Preview Help for feature: Description | |
| Delete | |
| String Parameter | |
| [Help] | |
| Name | |
| num_of_iterations | |
| Help for feature: Name | |
| Default Value | |
| 1 | |
| Help for feature: Default Value | |
| Description | |
| This value determines how many times <PRE> | |
| opam install $your_package | |
| </PRE>should be measured | |
| [Safe HTML] Preview Help for feature: Description | |
| Delete | |
| String Parameter | |
| [Help] | |
| Name | |
| coq_opam_packages | |
| Help for feature: Name | |
| Default Value | |
| coq-performance-tests coq-engine-bench coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-sf-plf coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast | |
| Help for feature: Default Value | |
| Description | |
| A space-separated list of OPAM packages whose installation you want to benchmark | |
| (at the HEAD of the branch and at the merge-base of the branch). | |
| Note that packages are topologically sorted by dependencies, but order is otherwise | |
| preserved. | |
| [Safe HTML] Preview Help for feature: Description | |
| Delete | |
| String Parameter | |
| [Help] | |
| Name | |
| new_ocaml_switch | |
| Help for feature: Name | |
| Default Value | |
| ocaml-base-compiler.4.07.1 | |
| Help for feature: Default Value | |
| Description | |
| The OCaml compiler used for the NEW branch. | |
| [Safe HTML] Preview Help for feature: Description | |
| Delete | |
| String Parameter | |
| [Help] | |
| Name | |
| old_ocaml_switch | |
| Help for feature: Name | |
| Default Value | |
| ocaml-base-compiler.4.07.1 | |
| Help for feature: Default Value | |
| Description | |
| The OCaml compiler used for the OLD branch. | |
| [Safe HTML] Preview Help for feature: Description | |
| Delete | |
| String Parameter | |
| [Help] | |
| Name | |
| coq_pr_number | |
| Help for feature: Name | |
| Default Value | |
| Help for feature: Default Value | |
| Description | |
| Only for use by coqbot. The PR number of the job to run. | |
| Overrides new_coq_repository, new_coq_commit, old_coq_repository, old_coq_commit with values fetched from GitHub. | |
| [Safe HTML] Preview Help for feature: Description | |
| Delete | |
| String Parameter | |
| [Help] | |
| Name | |
| coq_pr_comment_id | |
| Help for feature: Name | |
| Default Value | |
| Help for feature: Default Value | |
| Description | |
| Only for use by coqbot. A comment id to send to coqbot identifying which comment should be updated with performance information as the bench runs. | |
| [Safe HTML] Preview Help for feature: Description | |
| Delete | |
| Add Parameter | |
| Job Notifications | |
| Notification Endpoints | |
| Delete | |
| Format | |
| JSON | |
| Protocol | |
| HTTP | |
| Event | |
| All Events | |
| Job lifecycle event triggering notification | |
| URL | |
| https://webhooks.gitter.im/e/44218bd8b73caf0bcaed | |
| Help for feature: URL | |
| Where to send messages | |
| Timeout | |
| 30000 | |
| Help for feature: Timeout | |
| Timeout (in ms) | |
| Log | |
| 0 | |
| Number lines of log messages to send. Use -1 for all (use with caution). | |
| Add Endpoint | |
| Help for feature: Notification Endpoints | |
| Permission to Copy Artifact | |
| Rebuild options: Rebuild Without Asking For Parameters Help for feature: Rebuild options: | |
| Disable Rebuilding for this job | |
| Discard Old Builds Help for feature: Discard Old Builds | |
| Throttle Concurrent Builds | |
| Disable Build (No new builds will be executed until the project is re-enabled.) Help for feature: Disable Build (No new builds will be executed until the project is re-enabled.) | |
| Execute concurrent builds if necessary Help for feature: Execute concurrent builds if necessary | |
| Restrict where this project can be run Help for feature: Restrict where this project can be run | |
| Label Expression | |
| pendulum | |
| Help for feature: Label Expression | |
| Label is serviced by 1 node | |
| Advanced Project Options | |
| Advanced... | |
| Source Code Management | |
| None | |
| CVS | |
| CVS Projectset | |
| Git | |
| Subversion | |
| Build Triggers | |
| Trigger builds remotely (e.g., from scripts) Help for feature: Trigger builds remotely (e.g., from scripts) | |
| Build after other projects are built Help for feature: Build after other projects are built | |
| Build periodically Help for feature: Build periodically | |
| Poll SCM Help for feature: Poll SCM | |
| Build Environment | |
| Copy files into the job's workspace before building Help for feature: Copy files into the job's workspace before building | |
| Execute shell script on remote host using ssh Help for feature: Execute shell script on remote host using ssh | |
| SSH Agent | |
| Build | |
| Execute shell | |
| [Help] | |
| Command | |
| . ~/.opam/opam-init/init.sh | |
| ~/git/coq-bench/update.sh origin master | |
| ~/git/coq-bench/two_points_on_the_same_branch.sh | |
| See the list of available environment variables | |
| Delete | |
| Add build step | |
| Post-build Actions | |
| Add post-build action | |
| Save | |
| Apply | |
| Help us localize this pagePage generated: Jun 1, 2020 11:01:22 PMREST APIJenkins ver. 1.640 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment