Data

Tools

Indexes

Applications

Experiments

Open Source Science

https://github.com/agda/agda-ghc-names

Tool for making sense of the Haskell code generated by the Agda compiler

https://github.com/agda/agda-ghc-names

Science Score: 26.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • ○
    CITATION.cff file
  • ✓
    codemeta.json file
    Found codemeta.json file
  • ✓
    .zenodo.json file
    Found .zenodo.json file
  • ○
    DOI references
  • ○
    Academic publication links
  • ○
    Committers with academic emails
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (9.9%) to scientific vocabulary
Last synced: 11 months ago · JSON representation

Repository

Tool for making sense of the Haskell code generated by the Agda compiler

Basic Info
  • Host: GitHub
  • Owner: agda
  • License: mit
  • Language: Haskell
  • Default Branch: master
  • Size: 11.7 KB
Statistics
  • Stars: 4
  • Watchers: 30
  • Forks: 2
  • Open Issues: 0
  • Releases: 0
Created over 9 years ago · Last pushed over 9 years ago
Metadata Files
Readme License

README.txt 

MOTIVATION:
  When compiling Agda source via the current default backend MAlonzo,
  this generates Haskell code, with automatically generated Haskell
  identifiers of the shape ``MAlonzo.Code.MyHaskellisedModuleName.dXYZ''
  for Agda entities that translate to Haskell program-level variables.
  If the MAlonzo-generated Haskell is compiled for profiling,
  and run with profiling enabled, the GHC run-time system writes
  these identifiers to the *.prof (and *.hp) files.
  This makes direct inspection of *.prof files of limited use for the
  Agda developer. The tool ``agda-ghc-names fixprof'' included here
  translates these *.prof files to *.agdaIdents.prof,
  where each dXYZ is replaced with the Agda identifier it originates from.


agda-ghc-names extract 
  assumes that all *.hs files below  have been generated by MAlonzo,
  and extracts the mapping from their Haskell names to the original
  Agda names. Typically,  will be the --compile-dir argument
  used when compiling an Agda program.
  The mapping is saved in /agda-ghc-name-cache.dat .

  For a medium-size project, this requires around 3GB of heap space,
  and takes around 100 seconds.
  (The heavy heap usage is due to the use of haskell-src-exts
    for parsing the MAlonzo-generated Haskell files, which may be quite large.)

agda-ghc-names fixprof {+m} {+s}  .prof
  generates .agdaIdents*.prof by replacing Haskell identifiers
  in .prof by Agda identifiers, as far as these can be found
  in MAlonzo-compiled *.hs files below .
  This reads /agda-ghc-name-cache.dat if it already exists,
  and otherwise generates it in the same way as
  ``agda-ghc-names extract ''.
  The option ``+m'' includes also the original Haskell module column
  in the output.
  The option ``+s'' includes also the original Haskell source location column
  added in GHC-8 in the output.

agda-ghc-names find  {hsIdents}
  also reads /agda-ghc-name-cache.dat if it already exists,
  and otherwise generates it in the same ways as ``agda-ghc-names extract ''.
  Subsequently:
   * For each qualified Haskell identifier in {hsIdents}
     (which typically start with ``MAlonzo.Code.''),
     it prints the Agda identifiers corresponding to it.
     If {hsIdents} contains exactly one qualified identifier,
     then only the Agda identifier is printed;
     otherwise the mapping `` |-> ''
     is printed for each identifier given.
   * Each unqualified Haskell identifier in {hsIdents}
     is looked up in all module maps.
  If none are given on the command line, they are read from standard input.

agda-ghc-names find -m  {hsModNames}
  instead dumps the whole association list for each module specified.

Owner

  • Name: Agda Github Community
  • Login: agda
  • Kind: organization

GitHub Events

Total
Last Year

Committers

Last synced: about 1 year ago

All Time
  • Total Commits: 5
  • Total Committers: 2
  • Avg Commits per committer: 2.5
  • Development Distribution Score (DDS): 0.2
Past Year
  • Commits: 0
  • Committers: 0
  • Avg Commits per committer: 0.0
  • Development Distribution Score (DDS): 0.0
Top Committers
Name Email Commits
Wolfram Kahl k****l@c****a 4
Ulf Norell u****l@g****m 1
Committer Domains (Top 20 + Academic)
cas.mcmaster.ca: 1

Issues and Pull Requests

Last synced: about 1 year ago

All Time
  • Total issues: 0
  • Total pull requests: 0
  • Average time to close issues: N/A
  • Average time to close pull requests: N/A
  • Total issue authors: 0
  • Total pull request authors: 0
  • Average comments per issue: 0
  • Average comments per pull request: 0
  • Merged pull requests: 0
  • Bot issues: 0
  • Bot pull requests: 0
Past Year
  • Issues: 0
  • Pull requests: 0
  • Average time to close issues: N/A
  • Average time to close pull requests: N/A
  • Issue authors: 0
  • Pull request authors: 0
  • Average comments per issue: 0
  • Average comments per pull request: 0
  • Merged pull requests: 0
  • Bot issues: 0
  • Bot pull requests: 0
View more stats
Top Authors
Issue Authors
Pull Request Authors
Top Labels
Issue Labels
Pull Request Labels