8000 Fix & test `primShowNat` by lawcho · Pull Request #7500 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Fix & test primShowNat #7500

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
Merged
merged 2 commits into from
Sep 18, 2024
Merged

Fix & test primShowNat #7500

merged 2 commits into from
Sep 18, 2024

Conversation

lawcho
Copy link
Contributor
@lawcho lawcho commented Sep 18, 2024

This PR fixes primShowNat crashing at (JS) run-time, and updates the test suite to cover this.

@lawcho lawcho added backend: js JavaScript generation backend type: bug Issues and pull requests about actual bugs labels Sep 18, 2024
@andreasabel
Copy link
Member

Thanks!

Do you have the MWE that shows the crash? That would be great to have as testcase in test/Compiler/simple/.

@andreasabel andreasabel added this to the 2.8.0 milestone Sep 18, 2024
@andreasabel andreasabel added the pr: squash-me This PR needs squashing label Sep 18, 2024
@lawcho
Copy link
Contributor Author
lawcho commented Sep 18, 2024

Here is a MWE:

-- Tests primShowNat

module Issue7500 where

open import Agda.Builtin.Nat
open import Agda.Builtin.Unit
open import Agda.Builtin.String
open import Agda.Builtin.IO

postulate putStrLn : String → IO ⊤
{-# COMPILE GHC putStrLn = \ s -> putStrLn (Data.Text.unpack s) #-}
{-# COMPILE JS putStrLn = str => kt => kt(console.log(str)) #-}

main : IO ⊤
main = putStrLn (primShowNat 4)

Are you sure you want it in the test suite?
It adds 3.4 seconds, and is dominated by tests/Compiler/simple/Arith.agda (which is already very simple)

@andreasabel
Copy link
Member

Thanks!
I integrated the MWE into Arith.agda and reorganized the commits so that fix and test are in a single commit.

@andreasabel andreasabel added pr: preserve commits PR should be merged via rebase, preserving the commits and removed pr: squash-me This PR needs squashing labels Sep 18, 2024
@andreasabel andreasabel self-assigned this Sep 18, 2024
lawcho and others added 2 commits September 18, 2024 23:25
@lawcho @andreasabel
Document why not testing primShowChar
3414298
@lawcho @andreasabel
Fix primShowNat JS binding
8e12ee1 
and test primShowNat

Co-authored-by: Andreas Abel <andreas.abel@ifi.lmu.de>
Co-authored-by: Lawrence Chonavel <95857153+lawcho@users.noreply.github.com>
@andreasabel andreasabel merged commit 4b1da6a into agda:master Sep 18, 2024
9 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@andreasabel andreasabel andreasabel approved these changes

Assignees

@andreasabel andreasabel

Labels
backend: js JavaScript generation backend pr: preserve commits PR should be merged via rebase, preserving the commits type: bug Issues and pull requests about actual bugs
Projects
None yet
Milestone
2.8.0
Development

Successfully merging this pull request may close these issues.
2 participants
@lawcho @andreasabel
0