Skip to content
Snippets Groups Projects
  1. Dec 31, 2022
  2. Dec 30, 2022
  3. Dec 29, 2022
  4. Dec 28, 2022
  5. Dec 27, 2022
    • v-lafeychine's avatar
      chore(clippy): Fix clippy issues · 4ae08c19
      v-lafeychine authored
      4ae08c19
    • loutr's avatar
      fix(proost): change error display behaviour during file import · a7ce532f
      loutr authored and v-lafeychine's avatar v-lafeychine committed
      a7ce532f
    • v-lafeychine's avatar
      1e7e0448
    • v-lafeychine's avatar
      6c0a4d25
    • v-lafeychine's avatar
      5ec0294d
    • v-lafeychine's avatar
      chore(error): Add new method on Error · fa4c52b8
      v-lafeychine authored
      fa4c52b8
    • belazy's avatar
      Resolve "`whnf` doesn't unfold applications where the head is a declaration" ✨️ · 30fa4424
      belazy authored
      Closes #75 🐔️👍️
      
      🦀️🍰🦀️🍰🦀️🍰
      
      * chore(clippy): clippy
      
      * fix(kernel): unfold applications where the header is a `Decl`
      30fa4424
    • v-lafeychine's avatar
      Resolve "Make clippy annoying" ✨️ · b8a511d9
      v-lafeychine authored
      Closes #68 🐔️👍️
      Approved-by: default avatarbelazy <aarthuur01@gmail.com>
      Approved-by: default avatarloutr <loutr@crans.org>
      
      🦀️🍰🦀️🍰🦀️🍰
      
      * chore(nix): Bump dependencies
      
      * chore(clippy): Remove useless prefix/suffix (clippy::module_name_repetitions)
      
      * chore(clippy): Prevent failed fallback (clippy::default_fallback_numeric)
      
      * chore(parser): Modify parser hierarchy
      
      * fix(fmt): Reduce chain line to 90 columns
      
      * fix(proost): Fix documentation issues
      
      * fix(evaluator): Move out display function, since self is not used
      
      * chore(clippy): Use Self when possible (clippy::use_self)
      
      * fix(kernel): Use safe conversion char -> u8 instead
      
      * chore(clippy): Use explicit lifetime name (clippy::single_char_lifetime_names)
      
      * chore(clippy): Use explicit unreachable/control-flow operator when needed
      
      * chore(clippy): Use to_owned() when possible (clippy::inefficient_to_string + clippy::str_to_string)
      
      * chore(clippy): Use specific function for map function (clippy::map_unwrap_or + clippy::option_if_let_else)
      
      * chore(clippy): Use correct pattern-matching (clippy::pattern_type_mismatch)
      
      * chore(clippy): Apply must_use (clippy::must_use_candidate clippy::return_self_not_must_use)
      
      * chore(clippy): Modify two-arm matches into if-let (clippy::single_match_else)
      
      * fix(declaration): Made struct only-crate public
      
      * chore(clippy): Use const qualifier when possible (clippy::missing_const_for_fn)
      
      * chore(clippy): Use core instead of std (clippy::alloc_instead_of_core + clippy::std_instead_of_core)
      
      * chore(clippy): Inline format args (clippy::uninlined_format_args)
      
      * chore(clippy): Add LTO hints (clippy::missing_inline_in_public_items)
      
      * chore(clippy): [Non-test only] Remove wildcard import (enum_glob_use + wildcard_imports)
      
      * chore(clippy): Add semicolon when nothing is returned (semicolon_if_nothing_returned)
      
      * feat(clippy): Enable clippy lints
      
      * chore(workspace): Improve cargo workspace for dependencies
      b8a511d9
  6. Dec 24, 2022
    • aalbert's avatar
      Resolve "panic when entering "a"" ✨️ · f296610c
      aalbert authored
      Closes #71 🐔️👍️
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      
      🦀️🍰🦀️🍰🦀️🍰
      
      * feat(proost): add test for is_command behavior with 1 letter
      
      * fix(proost): add missing boundary check
      f296610c
    • belazy's avatar
      Resolve "Add Universe Polymorphism" ✨️ · 8b20ac80
      belazy authored and loutr's avatar loutr committed
      Closes #28 🐔️👍️
      Approved-by: default avatarbelazy <aarthuur01@gmail.com>
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarv-lafeychine <vincent.lafeychine@proton.me>
      Approved-by: default avatarloutr <loutr@crans.org>
      
      🦀️🍰🦀️🍰🦀️🍰
      
      * fix(proost): added Define command back (need to distinguish between the two in order to bind and reuse correctly later
      
      * chore(kernel, calculus/level): adapt documentation to new type
      
      * chore(level): Add specific enum to handle comparison state
      
      * chore(kernel): c-o-v-e-r-a-g-e
      
      * chore(parser): remove TODO
      
      * chore(parser): more coverage
      
      * fix(kernel): trailing comma when printing `InstantiatedDeclaration`s
      
      * fix(kernel): chiale + aboie, coverage
      
      * chore(kernel): mention #14
      
      * chore(kernel): yet another test
      
      * chore(kernel): always more coverage
      
      * chore(parser): add issue nb to todo
      
      * fix(kernel): avoid reentrant entry bug when infering type of decls with 0 universe arguments
      
      * fix(parser): revert comit, wtf clippy ?
      
      * chore(parser): remove unused branch
      
      * chore(kernel): another test
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * fix(kernel): remove dangerous function
      
      * chore(kernel): always more coverage
      
      * feat(parser): remove `Define` command
      
      * fix(kernel): interface checking for decls
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * chore(kernel): add coverage
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * chore(kernel): coverage
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * fix(kernel): over-agressive normalization
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * fix(parser): avoid spacing befor univ decls/vars
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * fix(proost): check existing identifiers for al definitions
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * feat(parser): add `DeclarationCheckType`
      
      * chore(kernel): remove unused test
      
      * fix(proost): type-check terms before `Eval`uating
      
      * docs: update
      
      * fix: further adjustments to parser
      
      * chore: formatting + some adjustments for kernel tests
      
      * fix(parser, proost): modify command generation for declarations
      
      * chore(parser): add tests todo
      
      * chore(parser): tests on sort parsing
      
      * fix(parser): tests
      
      * feat(parser): parse universe bindings
      
      * feat(parser): parse universe declarations in define_type
      
      * fix(level): comments
      
      * chore: remove biging as a dependency
      
      * chore(kernel): remove todo
      
      * chore(kernel): remove unused file
      
      * chore(kernel): more tests
      
      * chore(kernel): documentation of `level_builder.rs`
      
      * feat(kernel): tests coverage
      
      * fix(kernel): tests
      
      * feat(kernel/term/builder): add binding to (instantiated) declaration builders
      
      * feat(kernel): add builders for declaration
      
      * chore(kernel): refactor builder file hierarchy and simplify these files
      
      * fix(proost): some import errors
      
      * feat(parser): add parsing for univ parameters of definitions
      
      * chore(kernel): add todo
      
      * fix: remove lifetime dependency on LevelEnvironment
      
      * feat : add inference for declarations.
      
      * feat(parser): add new parsing rules for levels
      
      * feat(parser): new syntax for universe polymorphism
      
      * feat(kernel): add type-checking for Decls
      
      * feat: incorporate LevelBuilder in TermBuilder
      
      * fix(kernel): refactor impl organisation: unload most of arena's
      
      * WOOOHOOOO
      
      * fix(kernel, level): fix incorrect assignment in hashcons function
      
      * fix(kernel): more errors
      
      * feat(kernel): fixed some errors
      
      * feat(kernel): finish rudimentary bases for modifying parser and type checker
      
      * feat(kernel): further work on Levels
      
      * WIP feat(kernel): modify declaration.rs structure
      
      * fix(kernel): removing Dweller struct, using a macro instead
      
      * fix(kernel): refactor file structure to add new core types. first attempt for levels.
      
      * feat(kernel): add generic Dweller type
      
      * WIP fix(kernel): refactor file structure to add new core types
      
      * um
      
      * feat:something
      
      * AH
      
      * first commit
      8b20ac80
  7. Dec 17, 2022
  8. Dec 14, 2022
  9. Dec 04, 2022
    • loutr's avatar
      Resolve "Preparations for the first release" ✨️ · 74a80de4
      loutr authored
      Closes #48 🐔️👍️
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarv-lafeychine <vincent.lafeychine@proton.me>
      
      🦀️🍰🦀️🍰🦀️🍰
      
      * chore: change branch name mentions to main
      
      * feat(docs): add user manual
      
      * fix(rustyline): autocompletion format: bold -> grey
      
      * doc(all): add Proost logo
      
      * doc(rustyline_helper): minor URL adjustments
      
      * chore(README): update
      
      * feat(README): add Proost logo
      
      * feat(docs): add Proost logo in specification (LFS test in disguise)
      0.1.0
      74a80de4
    • v-lafeychine's avatar
      Resolve "Infrastructure improvement" ✨️ · bbdd1df8
      v-lafeychine authored and loutr's avatar loutr committed
      Closes #40 🐔️👍️
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarloutr <loutr@crans.org>
      
      🦀️🍰🦀️🍰🦀️🍰
      
      * chore(fmt): Modify format
      
      * chore(coverage): Tune branch + Include no_coverage feature
      
      * bump: Update pest to 2.5.1 and subdependencies
      
      * feat(cargo): Add licence check
      bbdd1df8
    • aalbert's avatar
      Resolve "Add file handling to proost" ✨️ · dc1fc185
      aalbert authored
      Closes #27, #29 et #36 🐔️👍️
      Approved-by: default avatarloutr <loutr@crans.org>
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarbelazy <aarthuur01@gmail.com>
      
      🦀️🍰🦀️🍰🦀️🍰
      
      * feat(parser): add tests
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * fix(kernel): fix tests
      
      * fix(kernel): fix tests
      
      * clippy
      
      * add tests
      
      * more tests
      
      * feat(proost): tests
      
      * clippy + move tests in kernel
      
      * repl -> evaluator
      
      * ex
      
      * change processor for repl
      
      * add verbose arg
      
      * remove deps
      
      * reference issues
      
      * add issue for search command
      
      * remove commandprocessor trait
      
      * rename repl.rs
      
      * fix error handling when failing to import file
      
      * fix(proost): consider suggestions from review; slight refactor of errors
      
      * chore(parser/commands): better display of the import command
      
      * chore(parser): renaming private functions and correcting some documentation
      
      * feat(proost): add better display for commands and use it instead in the import command display
      
      * fix(proost): adapt proost to new parser behaviour
      
      * fix(parser): make parser produce Builders instead of terms, which prevents evaluating commands too early
      
      * add basic search command
      
      * move pretty printing out of command processor
      
      * functional cyclic dependency test
      
      * better tab
      
      * still buggy, more tests
      
      * better emoji handling
      
      * import file 2/2
      
      * fix tests
      
      * clippy
      
      * import file 1/2: test if files exists
      
      * add convenient command for user
      
      * add import command, not fonctional yet
      
      * clippy
      
      * move command in parser
      dc1fc185
  10. Dec 01, 2022
  11. Nov 30, 2022
    • loutr's avatar
      Uniform Kernel Documentation ✨️ · 0d832e96
      loutr authored
      Closes #42 🐔️👍️
      Approved-by: default avatarbelazy <aarthuur01@gmail.com>
      Approved-by: default avatarv-lafeychine <vincent.lafeychine@proton.me>
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      
      🦀️🍰🦀️🍰🦀️🍰
      
      * chore(language): typo hunting
      
      * chore(kernel/type checker): adapt type checker tests to new kernel interface
      
      * chore(kernel/test): adapt `and.rs` test to new kernel interface
      
      * chore(proost): adapt proost to new kernel interface
      
      * chore(parser): adapt parser to new kernel interface
      
      * doc(kernel): complete documentation and interface
      
      * doc(kernel/builder): WIP
      
      * doc(kernel/calculus): complete documentation for calculus.rs
      
      * doc(arena): complete documentation for arena.rs
      
      * doc(kernel/arena): WIP
      0d832e96
  12. Nov 26, 2022
    • loutr's avatar
      Resolve "Refactor memory model of type checker" ✨️ · 066c0829
      loutr authored
      Closes #15 🐔️👍️
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarv-lafeychine <vincent.lafeychine@proton.me>
      Approved-by: default avatarbelazy <aarthuur01@gmail.com>
      
      🦀️🍰🦀️🍰🦀️🍰
      
      * chore(cargo): update
      
      * fix(from comments): second pass of small review changes
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * fix(kernel review): take Vincent comments into account
      
      * chore(cargo): update cargo.lock
      
      * fix(kernel tests): adapt to new builder structure
      
      * fix(proost): adapt proost toplevel to the new memory model.
      This includes a temporary solution for error management, which will be changed anyway.
      
      * fix(parser): adapt tests to memory model
      
      * fix(kernel): refactor build functions location
      
      * fix(parser): adapt parser to new model WIP
      
      * feat(builders): WIP rewriting builders
      
      * chore(file structure): reorganised the file structure of arena- or term-related functions
      
      * chore(terms): changing some annotations in the file
      
      * fix(tests): all tests now succeed. Errors were due to the rewriting of the tests, not the type checker
      
      * fix(terms): chose to modify Debug impl of Terms instead; which gives better, less verbose results
      
      * fix(terms): add wrapper around OnceCell in order to fix their Debug trait implementation (too enthusiastic by default)
      
      * fix(kernel): fix term generation error with depth, fix wrong imax computation in type inference, fix PartialEq impl for Node
      
      * fix(kernel tests): rewrite the and test
      
      * fix(commands): update commands and the associated other functions
      
      * fix(type checker): add necessary lifetime annotations on result
      
      * fix(kernel tests): refactor tests accordingly
      
      * feat(type checker): adapt type checking and errors to the memory model
      
      * fix(terms and type checker): use deref trait, further temporary changes in type checker, removing previous environment definition; early: won't compile
      
      * fix(terms): adapt all core functions from terms.rs; early: won't compile
      
      * fix(terms): fix lifetime issue; early; won't compile
      
      * feat(terms): finish new term description and generation
      
      * chore(cargo): add `im-rc` dependency for immutable structures
      066c0829
    • aalbert's avatar
      Resolve "improve README" ✨️ · dc410508
      aalbert authored and v-lafeychine's avatar v-lafeychine committed
      Closes #37 🐔️👍️
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarbelazy <aarthuur01@gmail.com>
      Approved-by: default avatarv-lafeychine <vincent.lafeychine@proton.me>
      
      🦀️🍰🦀️🍰🦀️🍰
      
      * add ?main
      
      * nix run
      
      * add backticks
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * fix links
      
      * add blabla
      
      * mermaid test
      
      * mermaid test
      
      * mermaid test
      dc410508
    • aalbert's avatar
      Resolve "Add functionnalities to proost (toplevel)" ✨️ · 1f0aa51e
      aalbert authored and v-lafeychine's avatar v-lafeychine committed
      Closes #39 🐔️👍️
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarv-lafeychine <vincent.lafeychine@proton.me>
      Approved-by: default avatarbelazy <aarthuur01@gmail.com>
      
      🦀️🍰🦀️🍰🦀️🍰
      
      * format
      
      * apply suggestion
      
      * clippy
      
      * apply suggestions
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * apply suggested change
      
      * apply suggestion
      
      * apply suggestions
      
      * add cmd option description
      
      * check if terminal and add option for syntax coloring
      
      * add tab
      
      * clippy fix
      
      * apply suggestion
      
      * fix coloring
      
      * apply suggestions
      
      * apply suggestions
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * add everything listed in issue except full multiline editing
      1f0aa51e
  13. Nov 10, 2022
    • aalbert's avatar
      Resolve "update specs" ✨️ · a28c6526
      aalbert authored
      Closes #35 🐔️👍️
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarloutr <loutr@crans.org>
      
      🦀️🍰🦀️🍰🦀️🍰
      
      * docs: fix example
      
      * docs: update README
      
      * docs: mentionning memory model + fix listing
      
      * feat(docs): correct examples
      
      * feat(docs): fix OCaml type and english
      
      * feat(docs): remove lfs
      
      * feat(docs): nixos+coverage
      
      * feat(docs): misc
      
      * feat(docs): add toplevel specs
      
      * feat(docs): update syntax
      
      * fix(tex): resolve listings errors
      
      * feat(docs): update specs
      a28c6526
  14. Nov 09, 2022
  15. Nov 04, 2022
    • v-lafeychine's avatar
      Resolve "Kernel errors" ✨️ · a636b12c
      v-lafeychine authored and loutr's avatar loutr committed
      Closes #19 🐔️👍️
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarbelazy <aarthuur01@gmail.com>
      Approved-by: default avatarloutr <loutr@crans.org>
      
      🦀️🍰🦀️🍰🦀️🍰
      
      * chore(Cargo.toml): Add a missing space
      
      * chore(ci): Remove unreachable line in coverage
      
      * chore(cargo): Improve dependencies with workspace feature
      
      * fix(ci): Tune coverage
      
      * chore: Cleaning tests
      
      * chore(kernel) : add coverage
      
      * fix(kernel) : add coverage tests
      
      * feat(errors): Improve errors handling
      
      * chore(rust): Use of Deref/DerefMut for Environment
      
      * chore(type_checker): Cleaning tests + Analyse branches
      
      * chore(error): Add Result type + Improve use
      
      * chore(location): Move location out of error file + Improve struct
      a636b12c
  16. Nov 01, 2022
    • aalbert's avatar
      Resolve " tests for parser" ✨️ · 328982eb
      aalbert authored
      Closes #8 🐔️👍️
      Approved-by: default avatarv-lafeychine <vincent.lafeychine@proton.me>
      Approved-by: default avatarbelazy <aarthuur01@gmail.com>
      
      🦀️🍰🦀️🍰🦀️🍰
      
      * feat(parser): resolve threads
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * feat(parser): resolve threads
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * feat(parser): more coverage
      
      * feat(parser): add one more test
      
      * feat(parser): add test for error conversion
      
      * feat(parser): more tests
      
      * feat(parser): more tests
      
      * feat(parser): more tests
      
      * feat(parser): first test
      328982eb
  17. Oct 29, 2022
  18. Oct 28, 2022
  19. Oct 27, 2022
    • aalbert's avatar
      Resolve "Bug rev parser" ✨️ · 1c6e1940
      aalbert authored
      Closes #30 🐔️👍️
      
      🦀️🍰🦀️🍰🦀️🍰
      
      * fix(parser)
      1c6e1940
    • v-lafeychine's avatar
      Resolve "proost fonctionality and UI" ✨️ · 1ffe4f63
      v-lafeychine authored and aalbert's avatar aalbert committed
      Closes #22 et #7 🐔️👍️
      Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
      Approved-by: default avatarbelazy <aarthuur01@gmail.com>
      Approved-by: default avatarloutr <loutr@crans.org>
      
      🦀️🍰🦀️🍰🦀️🍰
      
      * Chore : add test
      
      * Fix : shift vars when binding lambda-abstractions
      
      * fix(kernel): some tests were wrong
      
      * HOT fix(kernel): command definition fixed
      
      * HOT fix(parser): fix parenthesis
      
      * HOT fix(parser): order of fun
      
      * feat(parser): resolve threads
      
      * chore(parser): Merge renamed_rules on Error
      
      * chore(command): Merge Define/DefineCheckType + Add tests
      
      * chore(parser): apply suggestions
      
      * feat(parser): add location conversion from pest to proost's kernel
      
      * Apply 1 suggestion(s) to 1 file(s)
      
      * fix(all): resolve thread and change Pos for Loc (range position) +
      conversion from position to range position in parser
      
      * fix(all): resolve threads
      
      * feat(kernel): Add tests in commands.rs
      
      * feat(parser, error): add new errors for parser, pos struct, first use of pos and pretty print of parsing errors
      
      * feat(parser, kernel): new kernel error: cannot parse
      
      * feat(proost): new ui v1
      
      * feat(proost): new interface!
      
      * feat(parser, kernel): change grammar and pretty printing
      1ffe4f63
  20. Oct 24, 2022
Loading