deducteam/dedukti issues and pull requests

#333 - allow more letters in identifiers

Pull Request - State: closed - Opened by fblanqui 4 months ago

#332 - update syntax.bnf

Pull Request - State: open - Opened by fblanqui 4 months ago

#331 - ci: upgrade script + test various ocaml versions

Pull Request - State: closed - Opened by fblanqui 4 months ago - 6 comments

#330 - use open_[in|out]_bin instead of open_[in|out] (fix #329)

Pull Request - State: closed - Opened by fblanqui 4 months ago - 3 comments

#329 - error 'not a binary channel' on Windows

Issue - State: closed - Opened by fblanqui 4 months ago

#328 - ' not allowed at the beginning of an identifier

Issue - State: closed - Opened by fblanqui 7 months ago - 1 comment

#327 - See that non-referenced test leads to failed CI

Pull Request - State: closed - Opened by GuillaumeGen 12 months ago

#326 - Add check that all tests are mentionned in tests/main

Pull Request - State: closed - Opened by GuillaumeGen 12 months ago - 1 comment

#325 - Fix #295

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

#324 - Fix #318

Pull Request - State: closed - Opened by GuillaumeGen 12 months ago

#323 - Fix #319

Pull Request - State: closed - Opened by GuillaumeGen 12 months ago - 3 comments

#322 - parsing error

Issue - State: open - Opened by fblanqui 12 months ago

#321 - dk dep -s fails

Issue - State: open - Opened by fblanqui 12 months ago

#320 - dk --version doesn't work

Issue - State: closed - Opened by fblanqui 12 months ago - 1 comment

#319 - a thm must have a type

Issue - State: closed - Opened by fblanqui 12 months ago

#318 - dkcheck doesn't accept a rule LHS between parentheses

Issue - State: closed - Opened by fblanqui 12 months ago

#317 - feature request: option for not printing warnings

Issue - State: open - Opened by fblanqui about 1 year ago - 2 comments

#316 - Update tezt version

Pull Request - State: closed - Opened by GuillaumeGen about 1 year ago - 4 comments

#315 - Fix links

Pull Request - State: closed - Opened by GuillaumeGen about 1 year ago - 1 comment

#314 - Links seem to 404

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

#313 - Pragmas pretty printing

Pull Request - State: closed - Opened by specialfish9 over 1 year ago

#312 - Feature request: allowing local theorems

Issue - State: open - Opened by fblanqui almost 2 years ago - 2 comments

#311 - "Package conflict" when installing

Issue - State: closed - Opened by yoni206 almost 2 years ago - 2 comments

#310 - feature request: #REQUIRE module alias

Issue - State: open - Opened by fblanqui almost 2 years ago

#309 - Lexer: Fixes #308

Pull Request - State: closed - Opened by francoisthire about 2 years ago

#308 - Identifiers with single \ not accepted

Issue - State: closed - Opened by fblanqui about 2 years ago

#307 - More dks

Pull Request - State: closed - Opened by francoisthire about 2 years ago

#306 - Dkdep: Add a regression test for dkdep

Pull Request - State: closed - Opened by francoisthire about 2 years ago

#305 - Update dependencies

Pull Request - State: closed - Opened by francoisthire about 2 years ago

#304 - Dkdep: Make error message consistent

Pull Request - State: closed - Opened by francoisthire about 2 years ago

#303 - Erroneous suggestion from dk dep

Issue - State: closed - Opened by gabrielhdt about 2 years ago - 1 comment

#302 - Erroneous suggestion from dk dep

Issue - State: closed - Opened by gabrielhdt about 2 years ago - 1 comment

#301 - dk dep is too slow

Issue - State: open - Opened by fblanqui about 2 years ago

#300 - dk --version does not work

Issue - State: open - Opened by fblanqui over 2 years ago

#299 - Rules: Allow type annotations in higher-order patterns

Pull Request - State: closed - Opened by francoisthire over 2 years ago - 5 comments

#298 - Explicit require

Pull Request - State: closed - Opened by francoisthire over 2 years ago

#297 - Implement Dedukti standard

Pull Request - State: closed - Opened by francoisthire over 2 years ago

#296 - Fix filepath printing (fix #294)

Pull Request - State: closed - Opened by gabrielhdt over 2 years ago

#295 - Module identifier quoting

Issue - State: closed - Opened by gabrielhdt over 2 years ago

#294 - Path resolution

Issue - State: closed - Opened by gabrielhdt over 2 years ago

#293 - Rule typing failure

Issue - State: open - Opened by gabrielhdt over 2 years ago - 5 comments

#292 - Francois@more tezt 3

Pull Request - State: closed - Opened by francoisthire over 2 years ago

#291 - Tests: Move more tests to Tezt

Pull Request - State: closed - Opened by francoisthire over 2 years ago

#290 - Move all the basic OK tests to Tezt

Pull Request - State: closed - Opened by francoisthire over 2 years ago

#289 - Functionalisation of dependencies

Pull Request - State: closed - Opened by francoisthire over 2 years ago

#288 - Importation is done before type checking

Pull Request - State: open - Opened by francoisthire over 2 years ago

#287 - Introducing a toy example for the Dedukti's summer school

Pull Request - State: closed - Opened by francoisthire over 2 years ago - 1 comment

#286 - Command line manual is outdated

Issue - State: open - Opened by francoisthire over 2 years ago

#285 - Parameters not allowed in the declaration of a definable symbol

Issue - State: open - Opened by fblanqui over 2 years ago

#284 - Miscellaneous fixes

Pull Request - State: closed - Opened by gabrielhdt over 2 years ago

#283 - Pre Release 2.7

Pull Request - State: closed - Opened by gabrielhdt over 2 years ago

#282 - Add dependencies in dune-project

Pull Request - State: closed - Opened by gabrielhdt over 2 years ago

#281 - opam: Add missing dependencies

Pull Request - State: closed - Opened by francoisthire over 2 years ago

#280 - Kernel: Optimise conversion

Pull Request - State: closed - Opened by francoisthire over 2 years ago - 1 comment

#279 - Why Reduction.are_convertible_lst calls term_eq ?

Issue - State: open - Opened by fblanqui over 2 years ago - 5 comments

#278 - Update Tezt

Pull Request - State: closed - Opened by francoisthire over 2 years ago

#277 - All: Update OCaml version and Ocamlformat

Pull Request - State: closed - Opened by francoisthire over 2 years ago

#276 - New syntax for pragmas and assertions

Pull Request - State: open - Opened by dwarfmaster over 2 years ago - 3 comments

#275 - Add basic nix files to support developpement

Pull Request - State: closed - Opened by dwarfmaster over 2 years ago

#274 - Readme: Typos, install procedure

Pull Request - State: closed - Opened by gabrielhdt over 2 years ago

#271 - Install tezt.1.0.0 in CI

Pull Request - State: closed - Opened by gabrielhdt almost 3 years ago

#270 - Removing tezt patch from ci

Pull Request - State: closed - Opened by gabrielhdt almost 3 years ago

#267 - Update syntax.bnf + make bnf

Pull Request - State: closed - Opened by amelieled almost 3 years ago - 4 comments

#265 - Fix LRA and inconsistent capitalization

Pull Request - State: open - Opened by firewall2142 about 3 years ago

#261 - Question about #REQUIRE

Issue - State: open - Opened by fblanqui about 3 years ago - 3 comments

#253 - Some checklist on how to add non regression tests

Pull Request - State: closed - Opened by gabrielhdt about 3 years ago

#252 - Make Universo great again

Pull Request - State: closed - Opened by francoisthire about 3 years ago

#251 - Make universo compiles again

Pull Request - State: closed - Opened by francoisthire about 3 years ago

#250 - Dkmeta: Enhance the interface

Pull Request - State: closed - Opened by francoisthire about 3 years ago

#243 - Dkmeta: add more tests and bug fixes

Pull Request - State: closed - Opened by francoisthire over 3 years ago

#240 - Tezt: Initial setup

Pull Request - State: closed - Opened by francoisthire over 3 years ago

#239 - All: Use ocamlformat everywhere

Pull Request - State: closed - Opened by francoisthire over 3 years ago

#237 - Actions: Use actions instead of travis

Pull Request - State: closed - Opened by francoisthire over 3 years ago

#236 - Dkmeta: Prototype the integration test framework

Pull Request - State: closed - Opened by francoisthire over 3 years ago

#230 - Add universo to this repository

Pull Request - State: closed - Opened by francoisthire about 4 years ago

#229 - Add dkmeta in the repository

Pull Request - State: closed - Opened by francoisthire about 4 years ago

#224 - Is it possible to translate Coq to Isabelle (and Lean) using Dedukti?

Issue - State: open - Opened by brando90 over 4 years ago - 13 comments
Labels: question

#222 - Syntax fix.

Pull Request - State: closed - Opened by Gaspi over 4 years ago - 2 comments
Labels: question, behaviour improvement, Dedukti 2.7

#221 - matching: Fix the API issue and call the correct function

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

#194 - Remove dune warnings

Pull Request - State: closed - Opened by francoisthire over 5 years ago
Labels: Dedukti 2.7

#191 - Identifiers in Dedukti

Issue - State: open - Opened by francoisthire over 5 years ago
Labels: behaviour improvement

#190 - Another api

Pull Request - State: closed - Opened by francoisthire over 5 years ago - 8 comments
Labels: Dedukti 2.7

#187 - Fix parser handling of underscores

Pull Request - State: closed - Opened by Gaspi over 5 years ago - 1 comment
Labels: Dedukti 2.7

#179 - Syntax extension to allow any symbols

Pull Request - State: closed - Opened by Gaspi over 5 years ago
Labels: Dedukti 2.7

#171 - Functorize the rewrite engine of Dedukti (only modifications to the kernel)

Pull Request - State: closed - Opened by francoisthire over 5 years ago
Labels: Dedukti 2.7

#161 - More elementary function in the APi

Pull Request - State: closed - Opened by GuillaumeGen almost 6 years ago - 1 comment

#155 - Infer context had a weird behaviour in the case of non-linear rule

Pull Request - State: closed - Opened by GuillaumeGen almost 6 years ago

#154 - Rule_infos_to_typed_rule in typing.ml

Pull Request - State: closed - Opened by GuillaumeGen about 6 years ago

#153 - Export the signature

Pull Request - State: closed - Opened by GuillaumeGen about 6 years ago

#149 - Add a way to get a function definition

Pull Request - State: closed - Opened by francoisthire about 6 years ago

#148 - Flag to allow eta in conversion test

Pull Request - State: closed - Opened by Gaspi about 6 years ago - 1 comment

#147 - Nested comments

Pull Request - State: closed - Opened by GuillaumeGen about 6 years ago

#139 - Revert "Revert "[WIP] Removing Syntactic/MP distinctions""

Pull Request - State: closed - Opened by GuillaumeGen over 6 years ago

#138 - Revert "[WIP] Removing Syntactic/MP distinctions"

Pull Request - State: closed - Opened by francoisthire over 6 years ago

#136 - Moving library folder to root

Pull Request - State: closed - Opened by Gaspi over 6 years ago

#132 - [WIP] Removing Syntactic/MP distinctions

Pull Request - State: closed - Opened by Gaspi over 6 years ago

#131 - Implementing "lets" as syntactic sugar

Pull Request - State: closed - Opened by Gaspi over 6 years ago - 18 comments

#130 - Functorising the parser to easily parse strings

Pull Request - State: closed - Opened by GuillaumeGen over 6 years ago

#105 - Remove left-linearity checking (deprecates `-nl` option)

Pull Request - State: closed - Opened by francoisthire over 6 years ago - 9 comments

#100 - Install manpages for binaries

Issue - State: closed - Opened by Gbury over 6 years ago
Labels: enhancement

GitHub / deducteam/dedukti issues and pull requests