Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / math-comp/hierarchy-builder issues and pull requests

#461 - [CI] Update Nix toolbox

Pull Request - State: closed - Opened by proux01 7 days ago - 1 comment

#460 - Link to tutorial

Issue - State: open - Opened by CohenCyril 8 days ago

#459 - HB.howto does not find instances

Issue - State: open - Opened by Tragicus 10 days ago

#458 - Disactivate coqeal on master (currently broken)

Pull Request - State: closed - Opened by proux01 15 days ago - 1 comment

#457 - [CI] Update Nix toolbox

Pull Request - State: closed - Opened by proux01 15 days ago

#456 - HB.lock "erefl body" error message

Issue - State: open - Opened by hivert 20 days ago - 6 comments

#455 - HB does not preserve the name of implicit arguments

Issue - State: open - Opened by silene 20 days ago - 5 comments

#454 - remove buggy notation

Pull Request - State: open - Opened by gares 20 days ago

#453 - HB breaks the parsing of commas (tuples, "in" clauses, etc)

Issue - State: open - Opened by silene 21 days ago - 4 comments

#452 - Poor error message in case of nonexhaustive list of dependencies

Issue - State: open - Opened by silene 21 days ago - 1 comment

#450 - [CI] Add test-suite

Pull Request - State: closed - Opened by proux01 about 1 month ago - 1 comment

#449 - fix cat

Pull Request - State: open - Opened by CohenCyril about 1 month ago

#448 - Feature request: adding target to HB.instance

Issue - State: open - Opened by CohenCyril about 1 month ago - 3 comments

#447 - Cannot infer parameters

Issue - State: open - Opened by zstone1 about 2 months ago

#446 - Extra parameters in instances cause bad errors

Issue - State: open - Opened by zstone1 about 2 months ago

#445 - put factory-alias->gref in the database

Pull Request - State: closed - Opened by gares about 2 months ago

#444 - Make the code compatible with the new elpi file resolver

Pull Request - State: closed - Opened by gares 2 months ago - 2 comments

#443 - Fix for new coq-elpi resolver.

Pull Request - State: closed - Opened by gares 2 months ago - 2 comments

#442 - HB.instance not produced anymore

Issue - State: open - Opened by affeldt-aist 2 months ago

#441 - HB.saturate failure

Issue - State: open - Opened by affeldt-aist 2 months ago

#435 - FTR: A scenario where `HB.instance` is too eager to infer

Issue - State: open - Opened by affeldt-aist 4 months ago - 2 comments

#432 - Bogus error: The conclusion of a builder is a mixin whose parameters

Issue - State: open - Opened by gares 4 months ago - 2 comments

#394 - Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10

Issue - State: closed - Opened by rtetley about 1 year ago - 2 comments

#217 - HB.graph confused by using 1 module path component for nodes, instead of 2

Issue - State: closed - Opened by gares over 3 years ago - 2 comments

#100 - Inheritance of mathcomp's structures

Issue - State: closed - Opened by volodeyka over 4 years ago - 1 comment
Labels: wontfix

#100 - Inheritance of mathcomp's structures

Issue - State: closed - Opened by volodeyka over 4 years ago - 1 comment
Labels: wontfix

#99 - HB forgets about Canonical Instance

Issue - State: closed - Opened by volodeyka over 4 years ago - 4 comments
Labels: wontfix

#99 - HB forgets about Canonical Instance

Issue - State: closed - Opened by volodeyka over 4 years ago - 4 comments
Labels: wontfix

#98 - A bug with insertion of coercions

Issue - State: closed - Opened by dmitromikh over 4 years ago - 1 comment

#98 - A bug with insertion of coercions

Issue - State: closed - Opened by dmitromikh over 4 years ago - 1 comment

#97 - [hack] use Coq-Elpi elaborator to infer coercions

Pull Request - State: closed - Opened by gares over 4 years ago - 1 comment

#97 - [hack] use Coq-Elpi elaborator to infer coercions

Pull Request - State: closed - Opened by gares over 4 years ago - 1 comment

#96 - [coq-ci] update to Coq-Elpi 1.5

Pull Request - State: closed - Opened by gares over 4 years ago - 1 comment

#95 - Create main.yml

Pull Request - State: closed - Opened by gares over 4 years ago

#95 - Create main.yml

Pull Request - State: closed - Opened by gares over 4 years ago

#94 - [instance] typecheck the type first

Pull Request - State: closed - Opened by gares over 4 years ago

#94 - [instance] typecheck the type first

Pull Request - State: closed - Opened by gares over 4 years ago

#93 - Error message "BUG: ty-deps ..." should suggest to put `indexed` around the type

Issue - State: closed - Opened by gares over 4 years ago - 1 comment

#92 - coq-elpi 1.5

Pull Request - State: closed - Opened by gares over 4 years ago - 1 comment

#89 - outdated doc about builders

Issue - State: closed - Opened by gares over 4 years ago

#88 - in Coq 8.12 support #[local] HB.instance

Issue - State: closed - Opened by gares over 4 years ago - 1 comment

#87 - demo1 has still a dummy root structure with no properties

Issue - State: closed - Opened by gares over 4 years ago

#86 - In `HB.instance` force unification to extract the class instead of the second argument.

Pull Request - State: closed - Opened by CohenCyril over 4 years ago - 1 comment

#85 - Add an HB mode to generate mathcomp compat boilerplate

Issue - State: closed - Opened by CohenCyril over 4 years ago - 1 comment

#84 - HB.instance ty term should accept just the head symbol of ty

Issue - State: closed - Opened by gares over 4 years ago - 1 comment

#82 - adding is-structure

Pull Request - State: closed - Opened by CohenCyril over 4 years ago

#81 - refactoring/fixing phant-term build

Pull Request - State: closed - Opened by CohenCyril over 4 years ago

#80 - coq-elpi 1.4.1

Pull Request - State: closed - Opened by gares over 4 years ago - 2 comments

#79 - fixing missing typeabbrev from coq-elpi

Pull Request - State: closed - Opened by CohenCyril over 4 years ago - 4 comments

#78 - renaming factory-name

Pull Request - State: closed - Opened by CohenCyril over 4 years ago

#77 - Creating Left module on a Ring

Pull Request - State: closed - Opened by CohenCyril over 4 years ago

#76 - Coq master 0.9.1

Pull Request - State: closed - Opened by gares over 4 years ago

#75 - HB.instance Definition f A := .... A ....

Pull Request - State: closed - Opened by gares over 4 years ago - 1 comment

#74 - HB.instance Definition f Params := ... (outside a section)

Issue - State: closed - Opened by gares over 4 years ago - 1 comment

#73 - syntax HB.instance Definition := ...

Pull Request - State: closed - Opened by gares over 4 years ago - 5 comments

#72 - A brief report on trying to port the Iris hierarchy to HB

Issue - State: open - Opened by Janno over 4 years ago - 5 comments

#71 - simplify makefile

Pull Request - State: closed - Opened by gares over 4 years ago

#70 - port to coq-elpi 1.4

Pull Request - State: closed - Opened by gares over 4 years ago - 8 comments

#69 - Adapt to coq/coq#12267

Pull Request - State: closed - Opened by gares over 4 years ago - 1 comment

#68 - HB.builders should give access to names shadowed by the factory

Issue - State: closed - Opened by gares over 4 years ago - 1 comment

#67 - Factory fields now mask lemmas and operators by default

Pull Request - State: closed - Opened by CohenCyril over 4 years ago - 5 comments

#66 - Update docker-test.sh

Pull Request - State: closed - Opened by gares over 4 years ago - 1 comment

#65 - [feature] parameters in structures

Pull Request - State: closed - Opened by gares over 4 years ago - 7 comments

#64 - factoryname and factory-name types are too similar

Issue - State: closed - Opened by gares over 4 years ago

#63 - ci for coq master

Pull Request - State: closed - Opened by gares over 4 years ago

#62 - Generate an abbreviation `F X` for `F.axioms X` (fix #61)

Pull Request - State: closed - Opened by gares over 4 years ago - 2 comments

#61 - HB.structure Definition Ring := { A of SemiRing A & AbelianGroup A }

Issue - State: closed - Opened by gares over 4 years ago - 3 comments

#60 - trying a different matrix

Pull Request - State: closed - Opened by CohenCyril over 4 years ago

#59 - CI: test nix package

Pull Request - State: closed - Opened by gares over 4 years ago - 1 comment

#58 - rm papers

Pull Request - State: closed - Opened by gares over 4 years ago

#57 - Structure and deps

Pull Request - State: closed - Opened by gares over 4 years ago - 10 comments

#56 - refine syntax for structures

Pull Request - State: closed - Opened by gares over 4 years ago - 2 comments

#55 - Uniform the syntax of HB.structure and HB.mixin/factory

Issue - State: closed - Opened by gares over 4 years ago - 1 comment

#54 - syntax for parameters

Pull Request - State: closed - Opened by gares over 4 years ago - 2 comments

#53 - HB.instance Definition bla := Foo.Build T .... syntax

Issue - State: closed - Opened by gares over 4 years ago - 1 comment

#52 - HB.mixin should not rename the type variable

Issue - State: closed - Opened by gares over 4 years ago - 2 comments

#51 - Require Import hb and String scope.

Issue - State: closed - Opened by gares over 4 years ago

#50 - HB.structure should beta redute the type of exported ops

Issue - State: closed - Opened by gares over 4 years ago

#49 - HB.instance should check for duplicate mixins

Issue - State: open - Opened by gares over 4 years ago - 2 comments

#48 - Opam

Pull Request - State: closed - Opened by gares over 4 years ago

#47 - ci based on docker

Pull Request - State: closed - Opened by gares over 4 years ago

#46 - Depend on coq-elpi version 1.3

Pull Request - State: closed - Opened by gares over 4 years ago - 2 comments

#45 - Tentative roadmap

Issue - State: closed - Opened by gares over 4 years ago

#44 - Simplify README

Pull Request - State: closed - Opened by gares over 4 years ago

#43 - Fix math notations

Pull Request - State: closed - Opened by pi8027 almost 5 years ago

#42 - New syntax

Pull Request - State: closed - Opened by gares almost 5 years ago - 18 comments

#41 - [DRAFT] new syntax

Issue - State: closed - Opened by gares almost 5 years ago - 13 comments

#40 - elpi 1.10 does close programs in their definition environment

Pull Request - State: closed - Opened by gares almost 5 years ago

#39 - more refactoring

Pull Request - State: closed - Opened by CohenCyril almost 5 years ago - 4 comments

#38 - [wish] hb.generates

Issue - State: closed - Opened by gares almost 5 years ago - 1 comment

#37 - [wip] updating README

Pull Request - State: closed - Opened by gares almost 5 years ago

#36 - HB.instance should no rely on `std.findall` order

Issue - State: closed - Opened by gares almost 5 years ago - 1 comment

#35 - [hack] coercions in arg->term

Pull Request - State: closed - Opened by gares almost 5 years ago - 6 comments

#34 - HB. commands should insert coercions when necessary

Issue - State: closed - Opened by CohenCyril almost 5 years ago - 7 comments

#33 - Class of

Pull Request - State: closed - Opened by CohenCyril almost 5 years ago

#32 - shortenings + new instance Qc + bugfixes

Pull Request - State: closed - Opened by CohenCyril almost 5 years ago