Skip to content
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

Isabelle/HOL translation: recursive translation of the whole project #2977

Open
wants to merge 8 commits into
base: main
Choose a base branch
from
Open

Isabelle/HOL translation: recursive translation of the whole project #2977

wants to merge 8 commits into from

Conversation

lukaszcz
Copy link
Collaborator

@lukaszcz lukaszcz commented Aug 28, 2024 •
edited
Loading

Checklist

  • Pipeline infrastructure to process arbitrary Juvix pipelines recursively
  • CLI
  • Theory names
  • Qualified names
  • Qualified imports with alias

@lukaszcz lukaszcz added enhancement New feature or request backend:isabelle labels Aug 28, 2024
@lukaszcz lukaszcz added this to the 0.6.6 milestone Aug 28, 2024
@lukaszcz lukaszcz self-assigned this Aug 28, 2024
@lukaszcz lukaszcz mentioned this pull request Sep 2, 2024
Open
@lukaszcz lukaszcz marked this pull request as ready for review September 2, 2024 14:07
@lukaszcz
Copy link
Collaborator Author

lukaszcz commented Sep 3, 2024

The CI fails because of a bug in GHC:

[560 of 675] Compiling Juvix.Compiler.Backend.Isabelle.Translation.FromTyped
  
  <no location info>: error:
      panic! (the 'impossible' happened)
    GHC version 9.8.2:
  	lookupIdSubst
    $sgoExpression_sBxI4
    InScope {eta_B0 eta_B1 eta_B2 wild_X2 wild_X3 eta2_XE eta3_XF
             wild_XI wild_XJ wild_XL wild_XM wild_XN wild_XO go3_anFo
             $cfmap_aB3Vz $c<$_aB3VO cl_aB45G cls_aB45J p_aB45K pat_aB45T
             $d(%,%)_aB6o2 $d(%,%)_aB6o4 $d(%,%)_aB6o7 $d(%,%)_aB6of $krep_aB6qK
             $krep_aB6qL $krep_aB6qM $krep_aB6qN $krep_aB6qO $krep_aB6qP
             $krep_aB6qQ $krep_aB6qR $krep_aB6qS $krep_aB6qT $krep_aB6qU
             $krep_aB6qV $krep_aB6qW $krep_aB6qX $krep_aB6qY $krep_aB6qZ
             $krep_aB6r0 ds_dB8SV ds_dB8VC ds_dB8VZ ds_dB8W4 ds_dB8W5 wild_iklsw
             x1_iklsx x2_iklsy wild_iBak0 x2_iBak1 x3_iBak2 x4_iBak3 x5_iBak4
             x6_iBak5 x7_iBak6 x8_iBak7 x9_iBak8 x10_iBak9 x11_iBaka x12_iBakb
             x13_iBakc _nameMap _nameSet $tc'NameSet $tcNameSet $tc'NameMap
             $tcNameMap nameSet _nestedPatterns _nestedElem nameMap $tc'Nested
             $tcNested $fFunctorNested nestedElem nestedPatterns fromInternal
             goModule $trModule $trModule_sB9Vi $trModule_sB9Vk $krep_sB9Vl
             $krep_sB9Vm $krep_sB9Vn $tcNameSet_sB9Vp $tcNameSet_sB9Vq
             $tc'NameSet_sB9Vr $tc'NameSet_sB9Vs $tcNameMap_sB9Vt
             $tcNameMap_sB9Vu $tc'NameMap_sB9Vv $tc'NameMap_sB9Vw
             $tcNested_sB9Vx $tcNested_sB9Vy $krep_sB9Vz $krep_sB9VA $krep_sB9VB
             $krep_sB9VC $krep_sB9VD $tc'Nested_sB9VE $tc'Nested_sB9VF loc_sBa04
             loc_sBa05 loc_sBa06 $dIP_sBa08 $dIP_sBa09 loc_sBa0f $dIP_sBa0q
             $dIP_sBa0s loc_sBa10 $dIP_sBa12 $dIP_sBa13 $dIP_sBa16 loc_sBa1w
             loc_sBa1O $dIP_sBa1R $dIP_sBa1S $dIP_sBa1V fromInternal_sBcsZ
             $sinsert'_sBglX $sinsert'_sBglZ $s$winsert'_sBgmL $s$winsert'_sBgnf
             $s$wupdateOrSnocWithKey_sBgnn $slookup#_sBgnz $slookup#_sBgnO
             $shash_sBgnR $shash_sBgnT $sppTrace_sBgnY $sdoc_sBgo4 poly_f_sBgpe
             lvl_sBgpf lvl_sBgHJ poly_go1_sBgK3 poly_go1_sBgKz lvl_sBgNN
             lvl_sBgNO lvl_sBgNQ lvl_sBgNR reservedNames_sBgVC
             getPatternArgName_sBgVK goRecordFields_sBgVO
             goInductiveParameter_sBgW7 mkExprCase_sBgW9 lvl_sBgWc lvl_sBgWd
             lvl_sBgWe lvl_sBgWo toIsabelleTheoryName_sBgWu lvl_sBgWA lvl_sBgWS
             c_sBgYq go1_sBgYA go1_sBgYO go1_sBgZ6 go1_sBgZo lvl_sBgZG lvl_sBgZQ
             lvl_sBh05 quoteName_sBh12 loc_sBh1i loc_sBh1k loc_sBh1m $dIP_sBh1s
             $dIP_sBh1u unsupportedType_sBh1A lvl_sBh1E lvl_sBh1F lvl_sBh1J
             txt_sBh2M txt_sBh2X txt_sBh37 txt_sBh3i txt_sBh3F lvl_sBh3G
             loc_sBh3W loc_sBh3Y loc_sBh40 $dIP_sBh46 $dIP_sBh48 lvl_sBh49
             loc_sBh4S loc_sBh4U $dIP_sBh50 $dIP_sBh52 $dIP_sBh54 lvl_sBh5A
             lvl_sBh5B lvl_sBhda lvl_sBhez lvl_sBheA lvl_sBheB lvl_sBheC
             lvl_sBheF lvl_sBhf1 loc_sBhgk loc_sBhgm loc_sBhgt $dIP_sBhhL
             $dIP_sBhhR loc_sBhi9 loc_sBhie loc_sBhig $dIP_sBhik $dIP_sBhim
             $dIP_sBhio loc_sBhjM loc_sBhjO loc_sBhjQ $dIP_sBhjU $dIP_sBhk1
             $dIP_sBhk7 lvl_sBhmP lvl_sBhnD lvl_sBhoj lvl_sBhql lvl_sBhqm
             n_sBhzC n_sBhzN lvl_sBhA2 lvl_sBhAy lvl_sBhAG lvl_sBhAI lvl_sBhEi
             lvl_sBhEF lvl_sBhEH lvl_sBhEI lvl_sBhF7 lvl_sBhFH lvl_sBhFM n_sBhHV
             lvl_sBhIG lvl_sBhIM lvl_sBhIO lvl_sBhIP ds_sBhJ7 lvl_sBhJ9
             lvl_sBhJR lvl_sBhK4 lvl_sBhKi lvl_sBhKj lvl_sBhKv lvl_sBhKD
             lvl_sBhLa lvl_sBhMi $dIP_sBnQ3 $dIP_sBnQ8 $dIP_sBnQp $dIP_sBnR5
             $dIP_sBnRs $w$j2_sBrdt $wgoNestedBranches_sBreh $wunsafeDrop_sBreI
             $wfilterTypeArgs_sBrf5 $w$j2_sBrfP $wpoly_go2_sBrh6
             $wpoly_go1_sBrhr $wpoly_go2_sBri2 $wpoly_go1_sBrin
             $wlocalName_sBriJ $wpoly_go2_sBrj6 $wpoly_go1_sBrjq $wquote'_sBrjO
             $wtoIsabelleTheoryName_sBrlh $wquote_sBro6 $wquoteName_sBrtd
             $wpoly_go1_sBrwo $wlookupName_sBrxY $wlvl_sBrza ww_sBrBJ ww_sBrBK
             ww_sBrBL ww_sBrBQ onlyTypes_sBrGz infoTable_sBrGA ww_sBrGE ww_sBrGF
             ww_sBrGG $wgoModule_sBrGK $wfromInternal_sBrHo ww_sBrI1 ww_sBrI2
             ww_sBrI3 lvl_sBtCb lvl_sBtCc lvl_sBtCd lvl_sBtCe lvl_sBtCf
             lvl_sBtCg lvl_sBtCh lvl_sBtCi lvl_sBtCj lvl_sBtCk lvl_sBtCm
             lvl_sBtCn lvl_sBtCo lvl_sBtCp lvl_sBtCq lvl_sBtCr lvl_sBtCy
             lvl_sBtCz lvl_sBtCB lvl_sBtCC lvl_sBtCD lvl_sBtCE lvl_sBtCF
             lvl_sBtCM lvl_sBtCN lvl_sBtCP lvl_sBtCQ lvl_sBtCR lvl_sBtD0
             lvl_sBtD1 lvl_sBtD3 lvl_sBtD4 lvl_sBtD5 lvl_sBtDe lvl_sBtDf
             lvl_sBtDh lvl_sBtDi lvl_sBtDj lvl_sBtDs lvl_sBtDt lvl_sBtDw
             lvl_sBtDx lvl_sBtDy lvl_sBtDH lvl_sBtDI lvl_sBtDK lvl_sBtDL
             lvl_sBtDM lvl_sBtDN lvl_sBtDX lvl_sBtEa lvl_sBtEd lvl_sBtEe
             lvl_sBtEf lvl_sBtEo lvl_sBtEp lvl_sBtEs lvl_sBtEt lvl_sBtEu
             lvl_sBtED lvl_sBtEE lvl_sBtEG lvl_sBtEH lvl_sBtEI lvl_sBtEJ
             lvl_sBtEK lvl_sBtEL lvl_sBtEM lvl_sBtET lvl_sBtEU lvl_sBtEW
             lvl_sBtEX lvl_sBtEY lvl_sBtEZ lvl_sBtF0 lvl_sBtF9 lvl_sBtFc
             lvl_sBtFd lvl_sBtFe lvl_sBtFn lvl_sBtFr lvl_sBtFs lvl_sBtFv
             lvl_sBtFw lvl_sBtFD lvl_sBtFH lvl_sBtFI lvl_sBtFJ lvl_sBtFK
             lvl_sBtFL lvl_sBtFM lvl_sBtFN lvl_sBtFP lvl_sBtFQ lvl_sBtFS
             lvl_sBtFT lvl_sBtFU lvl_sBtFW lvl_sBtFX lvl_sBtFY lvl_sBtFZ
             lvl_sBtG0 lvl_sBtG1 lvl_sBtG2 lvl_sBtG3 lvl_sBtG4 lvl_sBtG8
             lvl_sBtG9 lvl_sBtGa lvl_sBtGh lvl_sBtGk lvl_sBtGl lvl_sBtGm
             lvl_sBtGn lvl_sBtGu lvl_sBtGv lvl_sBtGx lvl_sBtGy lvl_sBtGz
             lvl_sBtGA lvl_sBtGB lvl_sBtGG lvl_sBtGI lvl_sBtGL lvl_sBtGZ
             lvl_sBtH3 lvl_sBtH4 lvl_sBtHd lvl_sBtHh lvl_sBtHi go1_sBtHk
             go1_sBtHm xs_sBtHq go1_sBtHs poly_go_sBtHu lvl_sBtMB lvl_sBtMI
             lvl_sBtMK lvl_sBtMM lvl_sBtMO lvl_sBu1Z lvl_sBu2h lvl_sBu2J
             lvl_sBu37 lvl_sBu3u lvl_sBu3Q lvl_sBu4i lvl_sBu4I lvl_sBu54
             lvl_sBu5t lvl_sBu5P lvl_sBu6g lvl_sBu6E lvl_sBu7b lvl_sBu7D
             lvl_sBu8a lvl_sBu8B lvl_sBu91 $j_sBujL $j_sBujN lvl_sBujO lvl_sBujP
             lvl_sBujQ lvl_sBuk0 lvl_sBuk1 lvl_sBuk4 lvl_sBuk5 lvl_sBuk8
             lvl_sBul3 lvl_sBul7 lvl_sBul8 $j_sBulc lvl_sBule lvl_sBulx
             lvl_sBulM lvl_sBulN lvl_sBulO lvl_sBulP lvl_sBulU lvl_sBulV
             lvl_sBulW lvl_sBulX lvl_sBuqd lvl_sBuqg go1_sBurl go1_sBurt
             go1_sButz sc_sBxI1 sg_sBxI2 sg_sBxKz $sgo1_sBye2 $s$wpoly_go1_sByjA
             $s$wpoly_go2_sBykb $s$wpoly_go2_sBymZ $s$wpoly_go2_sByn0
             $s$wgo2_sByq6 $s$wgo2_sByqf $s$wgo2_sByqw $s$wgo2_sByqP
             $s$wgo2_sByqY $s$wgo2_sByrf $s$wgo2_sByry $s$wgo2_sByrH
             $s$wgo2_sByrY $s$wgo2_sBysh $s$wgo2_sBysq $s$wgo2_sBysH
             $s$wpoly_go1_sByHg $s$wpoly_go1_sByRu $s$wpoly_go1_sBySd
             $sgoRecordFields_sByTj $s$wgoNestedBranches'_sByTu $sgo1_sByTB
             lvl_sBz0D lvl_sBz0F mkIndType_sBz0H goType_sBz0J
             goRecordField_sBz0P lvl_sBz0R goConstructorDef_sBz0T lvl_sBz0V
             getList_sBz0X lvl_sBz0Z $wgetListPat_sBz11 names_sBz13
             disambiguate_sBz1e $wgoConstrName_sBz1g goPatternArgs_sBz1i
             $wgoNestedPattern_sBz1l goPatternArg_sBz1m $sgoPatternArg_sBz1n
             $wgoPatternArgCase_sBz6o $sgoExpression_sBz6q
             $sgoLambdaClauses_sBz6s $sgoExpression_sBz6t
             $sgoLambdaClauses_sBz6u goLambdaClauses_sBz6v goExpression_sBz6w
             $sgoLambdaClauses_sBz6x $sgoExpression_sBz6y sc_sBzm7 sc_sBzm8}
    Call stack:
        CallStack (from HasCallStack):
          callStackDoc, called at compiler/GHC/Utils/Panic.hs:191:37 in ghc-9.8.2-2c96:GHC.Utils.Panic
          pprPanic, called at compiler/GHC/Core/Subst.hs:197:17 in ghc-9.8.2-2c96:GHC.Core.Subst
    CallStack (from HasCallStack):
      panic, called at compiler/GHC/Utils/Error.hs:503:29 in ghc-9.8.2-2c96:GHC.Utils.Error
  
  Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug

The problem is with one of the optimizations (it works with optimizations turned off).

Possibly related:

@lukaszcz lukaszcz mentioned this pull request Sep 3, 2024
Merged
@lukaszcz lukaszcz modified the milestones: 0.6.6, 0.6.7 Sep 4, 2024
lukaszcz added a commit that referenced this pull request Sep 13, 2024
@lukaszcz @paulcadman
Update to GHC 9.10.1 (#2991)
87adaf4 
Since GHC 9.8.2 has a bug which blocks our development (see
#2977 (comment)), I
made a PR to update to GHC 9.10.1. Because stackage doesn't yet support
GHC 9.10.1, I had to add some explicit dependencies and use
`allow-newer-deps` in `stack.yaml`.

I think we should merge this not to get blocked by the bug, and later
clean up `stack.yaml` when GHC 9.10.1 becomes supported on stackage.

---------

Co-authored-by: Paul Cadman <[email protected]>
janmasrovira
janmasrovira previously approved these changes Sep 14, 2024
View reviewed changes
paulcadman
paulcadman requested changes Sep 14, 2024
View reviewed changes
Copy link
Collaborator

@paulcadman paulcadman left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We need to postpone merging this until I can resolve:

as we may need to rollback the GHC 9.10.1 upgrade if I cannot resolve it.

@lukaszcz lukaszcz mentioned this pull request Sep 18, 2024
Open
@paulcadman
Copy link
Collaborator

This PR is blocked until we can solve:

Which probably means we need to wait for stackage nightly to update to GHC 9.10.1.

@lukaszcz
Copy link
Collaborator Author

The problem persists with GHC 9.8.3

@paulcadman paulcadman modified the milestones: 0.6.7, 0.6.8 Nov 7, 2024
@paulcadman paulcadman modified the milestones: 0.6.8, 0.6.9 Nov 11, 2024
lukaszcz added a commit that referenced this pull request Nov 29, 2024
@lukaszcz @paulcadman
Update to GHC 9.10.1 (#2991)
342c820 
Since GHC 9.8.2 has a bug which blocks our development (see
#2977 (comment)), I
made a PR to update to GHC 9.10.1. Because stackage doesn't yet support
GHC 9.10.1, I had to add some explicit dependencies and use
`allow-newer-deps` in `stack.yaml`.

I think we should merge this not to get blocked by the bug, and later
clean up `stack.yaml` when GHC 9.10.1 becomes supported on stackage.

---------

Co-authored-by: Paul Cadman <[email protected]>
lukaszcz added a commit that referenced this pull request Nov 29, 2024
@lukaszcz @paulcadman
Update to GHC 9.10.1 (#2991)
2b1562a 
Since GHC 9.8.2 has a bug which blocks our development (see
#2977 (comment)), I
made a PR to update to GHC 9.10.1. Because stackage doesn't yet support
GHC 9.10.1, I had to add some explicit dependencies and use
`allow-newer-deps` in `stack.yaml`.

I think we should merge this not to get blocked by the bug, and later
clean up `stack.yaml` when GHC 9.10.1 becomes supported on stackage.

---------

Co-authored-by: Paul Cadman <[email protected]>
lukaszcz and others added 8 commits December 1, 2024 12:10
@lukaszcz
theory names
2164845
@lukaszcz
recursive translation
e0037c6
@lukaszcz
fix packages
17ec983
@lukaszcz
qualified names
f5150f7
@lukaszcz
use fully qualified names instead of aliases
2ec830e
@lukaszcz
fixes
bede889
@lukaszcz @paulcadman
Update to GHC 9.10.1 (#2991)
784e399 
Since GHC 9.8.2 has a bug which blocks our development (see
#2977 (comment)), I
made a PR to update to GHC 9.10.1. Because stackage doesn't yet support
GHC 9.10.1, I had to add some explicit dependencies and use
`allow-newer-deps` in `stack.yaml`.

I think we should merge this not to get blocked by the bug, and later
clean up `stack.yaml` when GHC 9.10.1 becomes supported on stackage.

---------

Co-authored-by: Paul Cadman <[email protected]>
@lukaszcz
fix Driver.hs
644d5a2
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@paulcadman paulcadman paulcadman requested changes

@janmasrovira janmasrovira janmasrovira left review comments

@jonaprieto jonaprieto Awaiting requested review from jonaprieto

Requested changes must be addressed to merge this pull request.

Assignees

@lukaszcz lukaszcz

Labels
backend:isabelle enhancement New feature or request
Projects
None yet
Milestone
0.6.9
Development

Successfully merging this pull request may close these issues.

Recursive Isabelle/HOL translation
3 participants
@lukaszcz @paulcadman @janmasrovira