[econstr] Flag to make `to_constr` fail if its output contains evars #6454

ejgallego · 2017-12-17T12:05:10Z

We forbid calling EConstr.to_constr on terms that are not evar-free,
as to progress towards enforcing the invariant that Constr.t is
evar-free. [c.f. #6308]

Due to compatibility constraints we provide an optional parameter to
to_constr, abort which can be used to overcome this restriction
until we fix all parts of the code.

Now, grepping for ~abort:false should return the questionable
parts of the system.

Not a lot of places had to be fixed, some comments:

problems with the interface due to Evd/Constr [Evd.define being
the prime example] do seem real!
inductives also look bad with regards to Constr/EConstr.
code in plugins needs work.

A notable user of this "feature" is Obligations/Program that seem to
like to generate kernel-level entries with free evars, then to scan
them and workaround this problem by generating constants.

SkySkimmer · 2017-12-17T12:27:26Z

Why is the commit from #6422 appearing?

SkySkimmer · 2017-12-17T12:28:08Z

I think abort should be called allow_undefined_evars or some such name which mentions evars.

SkySkimmer · 2017-12-17T12:38:51Z

vernac/himsg.ml

@@ -632,7 +632,8 @@ let explain_refiner_cannot_generalize env sigma ty =
  pr_leconstr_env env sigma ty ++ str "."

 let explain_no_occurrence_found env sigma c id =
-  let c = EConstr.to_constr sigma c in
+  (* XXX: Fixme *)
+  let c = EConstr.to_constr ~abort:false sigma c in
  str "Found no subterm matching " ++ pr_lconstr_env env sigma c ++


Why not use pr_leconstr here?

Indeed, I was hesitating at first whether to make this PR "tagging-only" or to also fix some trivial ocurrences. I guess it makes sense to fix a few, so I'll update this + I will change the name of the flag.

ejgallego · 2017-12-17T13:06:59Z

I think abort should be called allow_undefined_evars or some such name which mentions evars.

Good point, I wanted a very scary name as the idea is for the flag to go away, I'll give it another try.

maximedenes · 2017-12-19T23:30:26Z

It seems the linter fails.

ejgallego · 2017-12-20T10:16:03Z

Note that this PR implements a check that should be enabled in dev builds, but should be disabled in production IMO. So I dunno how to handle such stuff.

SkySkimmer · 2018-01-15T15:38:41Z

Note that this PR implements a check that should be enabled in dev builds, but should be disabled in production IMO. So I dunno how to handle such stuff.

Resurrect configure time -debug?
Instead of if abort then anomaly else constr.map use assert (not abort); constr.map and let production compilers use the option for removing asserts?

ppedrot · 2018-04-01T16:24:28Z

Sorry, I probably read too quickly "Enrico's PRs"! Anyways, this is still waiting for benching, I'll launch one.

ejgallego · 2018-04-01T16:44:07Z

Your job failed, relaunched: https://ci.inria.fr/coq/job/benchmark-part-of-the-branch/379/console

ejgallego · 2018-04-02T01:10:41Z

As the previous bench showed this seems to have no effect:

┌──────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┬─────────────────┐
│                          │      user time [s]      │              CPU cycles               │           CPU instructions            │  max resident mem [KB]  │   mem faults    │
│                          │                         │                                       │                                       │                         │                 │
│             package_name │     NEW     OLD PDIFF   │            NEW            OLD PDIFF   │            NEW            OLD PDIFF   │     NEW     OLD PDIFF   │ NEW OLD PDIFF   │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│         coq-fiat-parsers │  702.64  705.56 -0.41 % │  1944242465089  1952022781881 -0.40 % │  2968441445172  2974898695031 -0.22 % │ 3375280 3368228 +0.21 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│   coq-mathcomp-ssreflect │   44.52   44.70 -0.40 % │   122090496522   122127230081 -0.03 % │   142605909812   142738198718 -0.09 % │  537592  537720 -0.02 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│    coq-mathcomp-solvable │  202.61  203.34 -0.36 % │   560131475175   562892689583 -0.49 % │   766851472264   767845233678 -0.13 % │  867640  866844 +0.09 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│     coq-mathcomp-algebra │  185.63  186.21 -0.31 % │   513222460316   514758680688 -0.30 % │   689607598325   690090649915 -0.07 % │  644852  652380 -1.15 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│              coq-bignums │   79.99   80.23 -0.30 % │   220843409433   221385111565 -0.24 % │   284845475563   285943160726 -0.38 % │  525836  527212 -0.26 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│       coq-mathcomp-field │  464.46  465.51 -0.23 % │  1289456791636  1292238707089 -0.22 % │  2060663067397  2061431082946 -0.04 % │  814576  814472 +0.01 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│   coq-mathcomp-character │  275.74  276.23 -0.18 % │   764401132191   765308949205 -0.12 % │  1081752567818  1081720209372 +0.00 % │ 1072892 1072804 +0.01 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│    coq-mathcomp-fingroup │   64.42   64.52 -0.15 % │   177510316554   177269521890 +0.14 % │   235816900704   236075600008 -0.11 % │  593696  591044 +0.45 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                  coq-vst │ 3988.55 3990.72 -0.05 % │ 11087137041733 11095966829982 -0.08 % │ 14507392343260 14507541264340 -0.00 % │ 2227452 2224492 +0.13 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                coq-flocq │   63.16   63.18 -0.03 % │   174398751914   174213099526 +0.11 % │   211511001686   211764370148 -0.12 % │  661832  663840 -0.30 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│               coq-geocoq │ 3111.72 3109.22 +0.08 % │  8633385894577  8623069232610 +0.12 % │ 13803039094334 13801050240388 +0.01 % │ 1213332 1241464 -2.27 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│   coq-mathcomp-odd_order │ 1443.75 1442.21 +0.11 % │  4009861380670  4005594220364 +0.11 % │  6658548254231  6665233247749 -0.10 % │ 1360628 1411664 -3.62 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│      coq-formal-topology │   37.50   37.41 +0.24 % │   100469445456   100500075270 -0.03 % │   125471108773   125555941678 -0.07 % │  483668  483556 +0.02 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│             coq-compcert │  869.50  866.16 +0.39 % │  2408779668240  2400423285065 +0.35 % │  3429745544654  3429428213504 +0.01 % │ 1330484 1322400 +0.61 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│            coq-fiat-core │  111.46  110.86 +0.54 % │   309292551792   308416850840 +0.28 % │   377115991464   376846739602 +0.07 % │  502324  502368 -0.01 % │   0   0  +nan % │
├──────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-mathcomp-real_closed │  172.54  171.26 +0.75 % │   477293263956   474341816485 +0.62 % │   700157449499   700537525363 -0.05 % │  838244  843072 -0.57 % │   0   0  +nan % │
└──────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴─────────────────┘

ppedrot

OK for me.

ppedrot · 2018-04-04T11:35:19Z

@mattam82 Do you agree with the PR as it is currently? The changes in Obligations ought to be deferred to another PR, right?

@PierreCorbineau This PR is marginally related to Funind, do you want to make a particular comment on it anyways?

PierreCorbineau

I'm ok with it.

ppedrot · 2018-04-10T18:48:12Z

@mattam82 ping!

mattam82 · 2018-04-13T09:55:09Z

Yes, indeed, the changes should be deferred to antother PR. Green light on!

… contains evars

ejgallego · 2018-04-13T11:05:20Z

Cool! The effects of this patch are likely to be observed in the wild, so keep an eye folks.

SkySkimmer · 2018-04-13T11:07:19Z

Shouldn't this have had a dev/changes entry? It seems like something plugin developers should know about, and ocaml types won't tell them about it.

ppedrot · 2018-04-13T11:10:58Z

@SkySkimmer Not sure if it really deserves it, we keep changing the semantics of the ML API without care and so far people haven't punched us in the face yet. If you're concerned you can open another PR though...

ejgallego · 2018-04-13T11:17:12Z

@SkySkimmer I think you are right, I will push a PR.

[coq] Adapt to coq/coq#6454 "forbid calling to_constr on open terms"

… terms""

Revert "[coq] Adapt to coq/coq#6454 "forbid calling to_constr on open terms""

SkySkimmer reviewed Dec 17, 2017

View reviewed changes

ejgallego force-pushed the evar+strict_to_constr branch 5 times, most recently from bccdf47 to 5d79587 Compare December 18, 2017 16:22

maximedenes added the needs: fixing The proposed code change is broken. label Dec 19, 2017

ejgallego force-pushed the evar+strict_to_constr branch 9 times, most recently from a5b46ba to 1d512bc Compare December 29, 2017 15:51

ejgallego force-pushed the evar+strict_to_constr branch from 1d512bc to 995bbf3 Compare February 5, 2018 02:11

ejgallego force-pushed the evar+strict_to_constr branch 2 times, most recently from 1c5f6f0 to 8ea3b93 Compare February 12, 2018 17:28

ejgallego mentioned this pull request Feb 12, 2018

[econstr] Continue consolidation of EConstr API under interp. #6511

Merged

ejgallego force-pushed the evar+strict_to_constr branch 2 times, most recently from c0543b5 to ec46c61 Compare February 12, 2018 20:13

ejgallego modified the milestone: 8.9 Feb 13, 2018

ejgallego removed the needs: fixing The proposed code change is broken. label Apr 1, 2018

ppedrot removed the needs: benchmarking Performance testing is required. label Apr 2, 2018

ppedrot approved these changes Apr 2, 2018

View reviewed changes

ejgallego mentioned this pull request Apr 2, 2018

ssr: move/lemma takes much longer than move=>top; move: {top}(lemma top) #7133

Open

maximedenes approved these changes Apr 4, 2018

View reviewed changes

PierreCorbineau approved these changes Apr 8, 2018

View reviewed changes

ppedrot added the kind: cleanup Code removal, deprecation, refactorings, etc. label Apr 13, 2018

ppedrot merged commit 9f723f1 into coq:master Apr 13, 2018

ppedrot added a commit that referenced this pull request Apr 13, 2018

Merge PR #6454: [econstr] Flag to make to_constr fail if its output…

f3b84cf

… contains evars

ejgallego deleted the evar+strict_to_constr branch April 13, 2018 11:04

mattam82 added a commit to mattam82/Coq-Equations that referenced this pull request Apr 13, 2018

Merge pull request #55 from ejgallego/evar+strict_to_constr

a4b1c12

[coq] Adapt to coq/coq#6454 "forbid calling to_constr on open terms"

mattam82 added a commit to mattam82/Coq-Equations that referenced this pull request Apr 13, 2018

Revert "[coq] Adapt to coq/coq#6454 "forbid calling to_constr on open…

0e3bde6

… terms""

mattam82 added a commit to mattam82/Coq-Equations that referenced this pull request Apr 13, 2018

Merge pull request #72 from mattam82/revert-55-evar+strict_to_constr

8fb3d12

Revert "[coq] Adapt to coq/coq#6454 "forbid calling to_constr on open terms""

ejgallego mentioned this pull request Apr 16, 2018

Definition with wildcards generates anomaly "grounding a non evar-free term" #7265

Closed

ppedrot mentioned this pull request Apr 17, 2018

Guarded relies on non-ground EConstr #7286

Closed

This was referenced Apr 29, 2018

Constr/Econstr separation. #6258

Open

EConstr.to_constr considered harmful. #6308

Open

gares mentioned this pull request May 16, 2018

[ssr] fix after to_constr ~abort_on_undefined_evars was added #7524

Merged

SkySkimmer mentioned this pull request Jan 21, 2019

Fix #9344, #9348: incorrect unsafe to_constr in vnorm #9349

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[econstr] Flag to make `to_constr` fail if its output contains evars #6454

[econstr] Flag to make `to_constr` fail if its output contains evars #6454

ejgallego commented Dec 17, 2017 •

edited

Loading

SkySkimmer commented Dec 17, 2017

SkySkimmer commented Dec 17, 2017

SkySkimmer Dec 17, 2017

ejgallego Dec 17, 2017

ejgallego commented Dec 17, 2017

maximedenes commented Dec 19, 2017

ejgallego commented Dec 20, 2017 •

edited

Loading

SkySkimmer commented Jan 15, 2018

ppedrot commented Apr 1, 2018

ejgallego commented Apr 1, 2018

ejgallego commented Apr 2, 2018

ppedrot left a comment

ppedrot commented Apr 4, 2018

PierreCorbineau left a comment

ppedrot commented Apr 10, 2018

mattam82 commented Apr 13, 2018

ejgallego commented Apr 13, 2018

SkySkimmer commented Apr 13, 2018

ppedrot commented Apr 13, 2018

ejgallego commented Apr 13, 2018

[econstr] Flag to make to_constr fail if its output contains evars #6454

[econstr] Flag to make to_constr fail if its output contains evars #6454

Conversation

ejgallego commented Dec 17, 2017 • edited Loading

SkySkimmer commented Dec 17, 2017

SkySkimmer commented Dec 17, 2017

SkySkimmer Dec 17, 2017

Choose a reason for hiding this comment

ejgallego Dec 17, 2017

Choose a reason for hiding this comment

ejgallego commented Dec 17, 2017

maximedenes commented Dec 19, 2017

ejgallego commented Dec 20, 2017 • edited Loading

SkySkimmer commented Jan 15, 2018

ppedrot commented Apr 1, 2018

ejgallego commented Apr 1, 2018

ejgallego commented Apr 2, 2018

ppedrot left a comment

Choose a reason for hiding this comment

ppedrot commented Apr 4, 2018

PierreCorbineau left a comment

Choose a reason for hiding this comment

ppedrot commented Apr 10, 2018

mattam82 commented Apr 13, 2018

ejgallego commented Apr 13, 2018

SkySkimmer commented Apr 13, 2018

ppedrot commented Apr 13, 2018

ejgallego commented Apr 13, 2018

[econstr] Flag to make `to_constr` fail if its output contains evars #6454

[econstr] Flag to make `to_constr` fail if its output contains evars #6454

ejgallego commented Dec 17, 2017 •

edited

Loading

ejgallego commented Dec 20, 2017 •

edited

Loading