8000 Don't recompile if --keep-pattern-variables option changes · Issue #7059 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Don't recompile if --keep-pattern-variables option changes #7059

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
UlfNorell opened this issue Jan 12, 2024 · 2 comments · Fixed by #7060
Closed

Don't recompile if --keep-pattern-variables option changes #7059

UlfNorell opened this issue Jan 12, 2024 · 2 comments · Fixed by #7060
Assignees
@UlfNorell
Labels
ux: options Issues relating to Agda's command line options
Milestone
2.6.4.2

Comments

@UlfNorell
Copy link
Member

--keep-pattern-variables only affects interaction and should not require recompilation, but it's missing from

agda/src/full/Agda/Interaction/Options/Base.hs

Lines 1075 to 1091 in 561fdc2

recheckBecausePragmaOptionsChanged used current =
blankOut used /= blankOut current
where
-- "Blank out" irrelevant options.
-- It does not matter what we replace them with, so we take the null value.
blankOut opts = opts
{ _optShowImplicit = empty
, _optShowIrrelevant = empty
, _optVerbose = empty
, _optProfiling = empty
, _optPostfixProjections = empty
, _optCompileMain = empty
, _optCaching = empty
, _optCountClusters = empty
, _optPrintPatternSynonyms = empty
, _optShowIdentitySubstitutions = empty
}

@UlfNorell UlfNorell added the ux: options Issues relating to Agda's command line options label Jan 12, 2024
@UlfNorell UlfNorell added this to the 2.6.4.2 milestone Jan 12, 2024
@UlfNorell UlfNorell self-assigned this Jan 12, 2024
UlfNorell added a commit that referenced this issue Jan 12, 2024
@UlfNorell
add --keep-pattern-variables to options that don't require recompilation
5b80792 
fixes #7059
@UlfNorell UlfNorell mentioned this issue Jan 12, 2024
Merged
UlfNorell added a commit that referenced this issue Jan 12, 2024
@UlfNorell
add --keep-pattern-variables to options that don't require recompilat…
45146aa 
…ion (#7060)

fixes #7059
@nad
Copy link
Contributor
nad commented Jan 12, 2024

I was going to ask you to update the user manual, but apparently this option was incorrectly not included in the following list:

agda/doc/user-manual/tools/command-line-options.rst

Lines 1701 to 1759 in 45146aa

Agda records the options used when generating an interface file. If
any of the following options differ when trying to load the interface
again, the source file is re-typechecked instead:
* :option:`--allow-exec`
* :option:`--allow-incomplete-matches`
* :option:`--allow-unsolved-metas`
* :option:`--call-by-name`
* :option:`--cohesion`
* :option:`--confluence-check`
* :option:`--copatterns`
* :option:`--cubical-compatible`
* :option:`--cubical`
* :option:`--cumulativity`
* :option:`--double-check`
* :option:`--erase-record-parameters`
* :option:`--erased-cubical`
* :option:`--erased-matches`
* :option:`--erasure`
* :option:`--exact-split`
* :option:`--experimental-irrelevance`
* :option:`--flat-split`
* :option:`--guarded`
* :option:`--hidden-argument-puns`
* :option:`--infer-absurd-clauses`
* :option:`--injective-type-constructors`
* :option:`--instance-search-depth`
* :option:`--inversion-max-depth`
* :option:`--irrelevant-projections`
* :option:`--keep-covering-clauses`
* :option:`--local-confluence-check`
* :option:`--lossy-unification`
* :option:`--no-auto-inline`
* :option:`--no-eta-equality`
* :option:`--no-fast-reduce`
* :option:`--no-forcing`
* :option:`--no-guardedness`
* :option:`--no-import-sorts`
* :option:`--no-load-primitives`
* :option:`--no-pattern-matching`
* :option:`--no-positivity-check`
* :option:`--no-projection-like`
* :option:`--no-sized-types`
* :option:`--no-termination-check`
* :option:`--no-unicode`
* :option:`--no-universe-polymorphism`
* :option:`--omega-in-omega`
* :option:`--overlapping-instances`
* :option:`--prop`
* :option:`--qualified-instances`
* :option:`--rewriting`
* :option:`--safe`
* :option:`--save-metas`
* :option:`--syntactic-equality`
* :option:`--termination-depth`
* :option:`--two-level`
* :option:`--type-in-type`
* :option:`--warning`
* :option:`--without-K`

@UlfNorell
Copy link
Member Author

You mean it was correctly not added to the list, but incorrectly missing from the list in recheckBecausePragmaOptionsChanged.

AndrasKovacs pushed a commit that referenced this issue Jan 13, 2024
@UlfNorell @AndrasKovacs
add --keep-pattern-variables to options that don't require recompilat…
9bfbb26 
…ion (#7060)

fixes #7059
@andreasabel andreasabel modified the milestones: 2.6.5, 2.6.4.2 Feb 7, 2024
andreasabel pushed a commit that referenced this issue Feb 8, 2024
@UlfNorell @andreasabel
add --keep-pattern-variables to options that don't require recompilat…
3c35d3e 
…ion (#7060)

fixes #7059
VitalyAnkh pushed a commit to VitalyAnkh/agda that referenced this issue Mar 5, 2024
@UlfNorell @VitalyAnkh
add --keep-pattern-variables to options that don't require recompilat…
3cc1f61 
…ion (agda#7060)

fixes agda#7059
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 12, 2024
@UlfNorell @JobPetrovcic
add --keep-pattern-variables to options that don't require recompilat…
e8cdcde 
…ion (agda#7060)

fixes agda#7059
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@UlfNorell UlfNorell

Labels
ux: options Issues relating to Agda's command line options
Projects
None yet
Milestone
2.6.4.2
Development

Successfully merging a pull request may close this issue.

add --keep-pattern-variables to options that don't require recompilation agda/agda
3 participants
@nad @UlfNorell @andreasabel
0