| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
compatible change.
|
|
|
|
|
|
|
|
|
|
`make clean`.
|
|
|
|
|
|
These are also convenient from `vernac` [to be used in future PRs].
|
|
These are convenient to use `command.ml` for example.
We also fix a critical bug in the `fold_left_map` family of functions,
as witnessed by this old behavior.
```ocaml
fold_left2_map (fun c u v -> c+1,u+v) 0 [1;2;3] [1;2;3;];;
- : int * int list = (3, [6; 4; 2])
```
I have opted for a simple fix keeping the tail-recursive nature, I am
not in the mood of writing base libraries, but feel free to improve.
|
|
|
|
|
|
|
|
|
|
|
|
To fix #5081, that LtacProf associates time spent in tactic-evaluation
with the wrong tactic, I added two additional calls to the profiler
during tactic evaluation phase. These two calls do not update the call
count of the relevant tactics, but simply add time to them.
Although this fixes #5081, it introduces a new bug, involving tactics
which are aliases of other tactics, which I am not sure how to fix.
Here is the explanation of the issue, as I currently understand it (also
recorded in a comment in `profile_ltac.mli`):
Ltac semantics are a bit insane. There isn't
really a good notion of how many times a tactic has been "called",
because tactics can be partially evaluated, and it's unclear
whether the number of "calls" should be the number of times the
body is fetched and unfolded, or the number of times the code is
executed to a value, etc. The logic in `Tacinterp.eval_tactic`
gives a decent approximation, which I believe roughly corresponds
to the number of times that the engine runs the tactic value which
results from evaluating the tactic expression bound to the name
we're considering. However, this is a poor approximation of the
time spent in the tactic; we want to consider time spent evaluating
a tactic expression to a tactic value to be time spent in the
expression, not just time spent in the caller of the expression.
So we need to wrap some nodes in additional profiling calls which
don't count towards to total call count. Whether or not a call
"counts" is indicated by the `count_call` boolean argument.
Unfortunately, at present, we can get very strange call graphs when
a named tactic expression never runs as a tactic value: if we have
`Ltac t0 := t.` and `Ltac t1 := t0.`, then `t1` is considered to
run 0(!) times. It evaluates to `t` during tactic expression
evaluation, and although the call trace records the fact that it
was called by `t0` which was called by `t1`, the tactic running
phase never sees this. Thus we get one call tree (from expression
evaluation) that has `t1` calls `t0` calls `t`, and another call
tree which says that the caller of `t1` calls `t` directly; the
expression evaluation time goes in the first tree, and the call
count and tactic running time goes in the second tree. Alas, I
suspect that fixing this requires a redesign of how the profiler
hooks into the tactic engine.
|
|
We fix quite a few types, and perform some cleanup wrt to the
evar_map, in particular we prefer to thread it now as otherwise
it may become trickier to check when we are using the correct one.
Thanks to @SkySkimmer for lots of comments and bug-finding.
|
|
VS gitlab:
+ fiat-crypto (Circle has 4GB RAM, gitlab 2GB)
- caching opam (TODO)
- publishing artefacts (TODO)
* tests with -local, not installed
VS travis:
+ reusing build products
- flambda validate job (TODO?)
- OSX jobs (TODO at least check if free OSX is possible)
- linter (TODO?)
|
|
Namely:
- Set Printing Factorizable Match Patterns.
= Set Printing Allow Default Clause.
|
|
|
|
Moreover, when there are at least two clauses and the last most
factorizable one is a disjunction with no variables, turn it into a
catch-all clause.
Adding options
Unset Printing Allow Default Clause.
to deactivate the second behavior, and
Unset Printing Factorizable Match Patterns.
to deactivate the first behavior (deactivating the first one
deactivates also the second one).
E.g. printing
match x with Eq => 1 | _ => 0 end
gives
match x with
| Eq => 1
| _ => 0
end
or (with default clause deactivates):
match x with
| Eq => 1
| Lt | Gt => 0
end
More to be done, e.g. reconstructing multiple patterns in Nat.eqb...
|
|
This is to have a better symmetry between CCases and GCases.
|
|
Adding a space before the bar separating disjunctive patterns.
Removing an extra space after the bar for inner disjunctive patterns.
|
|
This reverts commit 5d4cf69a3d7d472b54b5decc8400164b87e9a73f.
|
|
|
|
This is a follow-up on 866b449c497933a3ab1185c194d8d33a86c432f2.
|
|
Program.Combinators
|
|
|
|
This way, `Time Show Ltac Profile` shows the profile in `*response*` in
PG, without an extra `infomsg` tag on the timing.
|
|
This fixes #6378. Previously the ML module was never declared anywhere.
Thanks to @cmangin for the pointer.
|
|
|
|
Revert "CI: poc Circleci configuration"
Committed on master by mistake. Clearly I'm too clumsy to be trusted
with push rights.
This reverts commit d606a85d53fbd0227b15e18701e2ac4c9d911f34.
CI: poc Circleci configuration
Fixup
Try minimising build for faster testing
Various fixes
Fixup: yaml identation
Do not -j2: native compiler seems to take too much memory
Revert "Do not -j2: native compiler seems to take too much memory"
This reverts commit 4886151288a8d895c0fd23f9bded0970c59e1372.
Deactivate native compiler
Fixup (how did this happen?)
Do not call time (not install on docker images, will fix later)
Fixup
Fixup
|
|
Fixes GH#6384 and GH#6385.
|
|
|
|
|
|
|
