Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://github.com/agda/agda/issues/7531 below:

JS backend crashes on big case split · Issue #7531 · agda/agda · GitHub

The JS backend has trouble compiling this code:

open import Agda.Builtin.Bool

data Cell : Set where
  [-] [o] [x] : Cell

data Board : Set where
  mk-Board : (
    _ _ _
    _ _ _
    _ _ _ : Cell)
    → Board 

game-over : Board → Bool
game-over = λ where
  (mk-Board [x]  _   _
            [x]  _   _
            [x]  _   _  ) → true

-- On an un-modified version of this file, `agda --js` takes
-- 0.01s and 0.03GB of RAM

  -- (mk-Board  _  [x]  _
  --            _  [x]  _
  --            _  [x]  _  ) → true

-- With all the cases above un-commented, `agda --js` takes
-- 0.01s and 0.03GB of RAM

  -- (mk-Board  _   _  [x]
  --            _   _  [x]
  --            _   _  [x] ) → true

-- With all the cases above un-commented, `agda --js` takes
-- 0.02s and 0.03GB of RAM

  -- (mk-Board [x] [x] [x]
  --            _   _   _
  --            _   _   _  ) → true

-- With all the cases above un-commented, `agda --js` takes
-- 0.1s and 0.05GB of RAM


  -- (mk-Board  _   _   _
  --           [x] [x] [x]
  --            _   _   _  ) → true
  

--  With all the cases above un-commented, `agda --js` takes
--  0.5s and 0.1GB of RAM


  -- (mk-Board  _   _   _
  --            _   _   _
  --           [x] [x] [x] ) → true

--  With all the cases above un-commented, `agda --js` takes
--  2.7 s and 0.5 GB of RAM

  -- (mk-Board [x]  _   _
  --            _  [x]  _
  --            _   _  [x] ) → true


--  With all the cases above un-commented, `agda --js` takes
--  >30s and >30GB of RAM
--  and crashes the OS.

  (mk-Board  _   _   _
             _   _   _
             _   _   _  ) → false

The crash occurs regardless of whether I define Board using data or record.

The crash does not occur with the GHC backend (even with 2x the number of cases).

This crash occurs with many Agda versions (both old and new):

• 1a711a4: Current tip of Fix #7508: remove unused-arg optimization from the JS backend #7509
• abd8a8e: Recent master
• b499d12: Agda v2.6.3

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4