docker: build-box should set opam env#6
Closed
fdupress wants to merge 1 commit into
Closed
Conversation
Member
|
Why? We're only installing stuffs in the switch, not using programs installed in the switch. |
Member
Author
|
This is for use of the build-box as a base for artefact boxes. Is there a
reason for not doing it?
…On Fri, 16 Mar 2018 at 06:23 Pierre-Yves Strub ***@***.***> wrote:
Why? We're only installing stuffs in the switch in this command.
—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
<#6 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AFyP3GDIpiXF8o9Ru7nfq6etyC2h7jPgks5te1pJgaJpZM4SsUtU>
.
|
Member
|
Each docker RUN starts a new shell. So you won’t inherit this eval in the subsequent docker RUN. |
Member
Author
|
Right. Sorry. The issue I was trying to get around with this is in fact due to something completely different: the fact that opam initialisation scripts are only run in login shells. Closing this and trying to think of another way of dealing with this. |
strub
added a commit
that referenced
this pull request
Apr 30, 2026
…hange) Splits the existing TcCtt resolution logic into three named local helpers — strat_tvar_via_tvtc, strat_abs_via_decl, strat_infer_by_carrier — corresponding to catalog modes #5, #6, and #1/#2 in doc/typeclasses-inference.md. Behavior is identical: same dispatch order, same failures, same pickup of [Tvar a]/[Tconstr p] cases, same parking of univar carriers. The refactor exists so Phase 3 can drop a By-args strategy in without disturbing the existing logic.
strub
added a commit
that referenced
this pull request
May 4, 2026
Two fixes in the typeclass inference layer that, together with the TcRing.ec authoring fixes (`ffield <: idomain`), let the file compile end-to-end: 1. ecProofTyping.pf_check_tvi was using only [EcTypeClass.infer] (which queries the instance database) to validate explicit tvi. That rejected ground but [\`Abstract]-typed carriers whose TC constraint chain reaches the queried class through inheritance — e.g. [eqr_div<:f>] where [f <: ffield <: idomain] and [eqr_div] needs [\`a <: idomain]. Add an [abs_satisfies] check that walks [EcTypeClass.ancestors] over each declared TC of the abstract type, mirroring [strat_abs_via_decl] (Mode #6) of the unifier. 2. ecTypeClass.TyMatch.doit_type used [Option.get (Mid.find_opt a map)] in the [Tvar a] case, which crashes the inference loop with [Invalid_argument "option is None"] when the pattern carries a free Tvar that isn't a tparam of the candidate instance (e.g. a section-local tparam that didn't get generalised). Treat such Tvars as a non-match. 3. examples/tcstdlib/TcRing.ec: declare [ffield <: idomain] (was [<: comring]) — fields are integral domains, matching main's theories/algebra/Ring.ec where [Field clone include IDomain].
strub
added a commit
that referenced
this pull request
May 7, 2026
[EcTypeClass.infer] previously consulted only the registered instance database, so its recursion in [check_tcinstance] (when matching a parametric instance, line 144) could not discharge a tparam constraint whose carrier was a section-declared abstract type. Concretely: section. declare type c <: comring. lemma _ (a b : c) : a + b = b + a. proof. apply (addrC<:c> a b). qed. failed with "type c does not satisfy typeclass constraint addgroup", because [check_constraints]' fallback to [abs_satisfies] is only a yes/no check and is not propagated through the recursive [infer] call inside parametric-instance matching. [EcUnify] handled this case via [strat_abs_via_decl] (Mode #6) in its strategy dispatch, but [EcTypeClass.infer] is called from several other paths (proof-term TVI elaboration, theory-replay, reduction) that don't go through the unifier dispatch. This adds [infer_via_abs_decl] alongside [check_tcinstance] and makes [infer] fall back to it after the instance-database search. The fallback walks [tcs] (the carrier's declared class bounds) looking for one whose ancestor DAG reaches [tc], and produces a [TCIAbstract { support = `Abs p; offset; lift }] witness — same shape as Mode #6 in [EcUnify]. Validates: the suite (TcMonoid/TcRing/TcInt/TcBigop/TcBigalg/ TcNumber/TcPoly) passes unchanged; new test [apply (addrC<:c> a b)] inside [section ; declare type c <: comring] now succeeds. Note: this fix completes constraint resolution for non- parametric Path B uses (e.g. [addrC<:c>]). The parametric case [addrC<:c poly>] now passes constraint resolution but the proof-term and goal witness encodings can still mismatch (the unifier produces a [TCIUni] with [lift] that doesn't always collapse to the goal's resolved form). That's a separate issue, untouched by this commit.
strub
added a commit
that referenced
this pull request
May 7, 2026
Closes the parametric-Path-B witness encoding gap that left class- lemma applications at parametric carriers ([apply (addrC<:c poly>)] inside [section ; declare type c <: comring]) unusable. **The bug.** [opentvi] creates a [TCIUni] for each opened tparam's TC bound and posts a [`TcCtt] problem, but doesn't itself drain the queue. The TCIUni stays parked in [tcenv.problems] until something else triggers [unify_core]. Meanwhile a proof-term carrying [(+)<:c poly[TCIUni #a [0;0]]>] arrives at the matcher's [try_delta], which tries [Op.tc_reducible env (+) tys] — and [tc_core_reduce] raises [NotReducible] on TCIUni witnesses, since it can only walk [TCIConcrete]/[TCIAbstract] forms. So [try_delta] falls through to [default]'s [is_conv], which doesn't TC-reduce either; matching fails, [pf_form_match] raises MatchFailure, [t_apply] reports "the given proof-term proves: ... it does not apply to the goal". **The fix.** Two changes: 1. [EcUnify.UniEnv.flush_tc_problems env ue] (new): runs [Unify.unify_core] on a trivial-true [`TyUni] problem, which re-pushes every parked [`TcCtt] in [tcenv.problems] and lets the strategy dispatcher resolve them. After the call, the resolution map contains a witness for every [TCIUni] that any strategy (Modes #1..#6) could pin. 2. In [EcMatching.f_match_core]'s [try_delta]: before destructuring the heads, call [flush_tc_problems env ue] and re-normalise both sides via [norm]. The substitution machinery in [tcw_subst] (ecCoreSubst.ml:209) dereferences resolved TCIUnis through [fs_tw_uni], so after [norm] both forms carry the concrete witness; [tc_reducible] then succeeds and [doit_tc_reduce] produces the renamed structural op (e.g. [polyD] for poly's addgroup-via-class-(+)), which conv'ing against the goal succeeds. Combined with the earlier framework fixes [0dd7d21] (infer-via- abs-decl) and [c182895] (alpha-equivalent chain reuse), this lets [apply (addrC<:c poly> p q)] and [apply (mulrA<:c poly> p q r)] inside a [c <: comring] section discharge directly, without requiring users to fall back to the underlying [polyD_addrC<:c>] / [polyM_mulrA] structural lemmas. The TcPoly port's structural-form workaround in Phase 6 / Phase 7 / smoke test stays as-is for the already-written code, but new code can use the natural class form. Validates: tcalgebra suite (TcMonoid/TcRing/TcInt/TcBigop/TcBigalg/ TcNumber/TcPoly/TcPolySmokeTest) all pass; the parametric Path B reproducer at /tmp/repro_pathb.ec now closes [test_path_b] via [apply (addrC<:c poly>)] without admit.
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.