First Pull Request

Adding exercises braibant/coq-tutorial-ml-tactics

We should add some exercises in a true "Software Foundation" spirit. - For instance, adding support for mult and minus - Adding an example of real reflexive decision/simplification procedure

Created - 0 comments - easy

Feature request: even stricter subproofs coq/coq

`Set Bullet Behavior` should accept an argument named something like `"Enforce Subproofs"`. When this option is active, proofs must be bullet-structured throughout. That is, whenever more than one ...

Created - 1 comment - good first issue kind: feature

[trivial] Fix the name of a test suite ocsigen/lwt

[It should be `lwt_list`, not `lwt_util`]( See [`](

Created - 1 comment - easy

tailrec versions of some of the list functions c-cube/ocaml-containers

- `CCList.split` - `CCList.combine`

Created - 1 comment - easy enhancement

Make Lwt.pick [] raise Invalid_argument ocsigen/lwt

This issue is about adding an `if` to [`Lwt.pick`][pick], [`Lwt.choose`][choose], [`Lwt.npick`][npick], [`Lwt.nchoose`][nchoose], and [`Lwt.nchoose_split`][nchoose_split], so that they raise `Inval...

Created - 1 comment - breaking easy enhancement good first issue

Comments dropped from files consisting of only comments ocaml-ppx/ocamlformat

Files that contain only comments have no parsetree locations at all, which defeats the comment placement algorithm. It seems that comment-only files need to be specifically recognized and all the c...

Created - 1 comment - bug good first issue

UI: TextInput component briskml/brisk

Similar to what we have with `TextView`, we need a `TextInput` component for entering text.

Created - 1 comment - good first issue help wanted macOS

Unneeded 'total' member in DieResult PrattFall/DiceCaddy

DieResult.t contains `total` member which could easily be replaced with a sum calculation on DieResult.values.

Created - 1 comment - good first issue

document the *.glob file format coq/coq

Note: the issue was created automatically with bugzilla2github tool Original bug ID: BZ#4834 From: @siegebell Reported version: unspecified CC:

Created - 2 comments - good first issue kind: documentation

F* wrongly allows non-linear patterns FStarLang/FStar

Recently discovered with @kyoDralliam that F* allows non-linear patterns: ``` let foo() : Tot int = match (1,2) with | (x,x) -> x ``` This is hugely unintuitive for users. Is this match c...

Created - 2 comments - area/error-messages area/usability good first issue kind/enhancement

META file is not installed in /usr/lib/ocaml coq/coq

<!-- Thank you for your contribution. Please complete the following information when reporting a bug. --> Following-up on #7296 but with a slightly different issue with META files #### Ve...

Created - 2 comments - good first issue part: installation

[easy-ish] Tests for Lwt_sequence ocsigen/lwt

[`Lwt_sequence`]( doesn't have a test suite at all, but it is [not immune to potential ser...

Created - 2 comments - easy good first issue technical debt

[easy] Delete Camlp4 from the manual introduction ocsigen/lwt

The Camlp4 syntax is deprecated, but we are still confusing users by [talking about it (at length) on the manual intro page (link; section "The syntax extension")](

Created - 2 comments - docs easy

Completely ignore any dependencies that don't have an "esy" field in package.json. esy/esy

This is a Good First Task for anyone looking to help out. We should ignore any dependencies (even dev dependencies) that don't have an `esy` field in their `package.json`. If we encourage people...

Created - 2 comments - enhancement good first issue

Remove SMTPatT FStarLang/FStar

The difference between `SMTPat` and `SMTPatT` is unclear since F* moved started using universes rather than the stratified type checker (see #547). @nikswamy said `SMTPatT` is around for backwar...

Created - 3 comments - area/syntax area/usability good first issue kind/enhancement

Point to from docs ocsigen/lwt

[]( was just launched as an experimental service. There's a bit of a (IMHO misguided) rush to create new categories (see e.g. the one for Core/Async), ...

Created - 3 comments - docs easy

jbuilder and the paths of Lwt's installed cmi files ocsigen/lwt

@diml in > qcow-tool fails to build in one the datakit build. I check, it's because mirage-block-unix uses Lwt_unix but...

Created - 3 comments - easy

Binding for ElementHandle.contentFrame() zploskey/bs-puppeteer

This should be included in Puppeteer 1.1.2 which is expected to be released on March 15th. [Docs](

Created - 3 comments - enhancement good first issue help wanted

Automatically configure "install" commands for package with *.install file present esy/esy

If a package has a single `*.install` file in the source tree and don't have `"esy.install"` configuration in `package.json` then we could configure `"esy.install"` to be `esy-installer` invocation...

Created - 4 comments - good first issue

Floating point literals are badly handled by the F# extraction mechanism FStarLang/FStar

Using literal floating point in some meant-to-be-extracted file like the F* compiler can produce bad results when extracting with the F# version of the F* compiler (seems to be fine with the ocaml ...

Created - 5 comments - area/fsharp-vs-ocaml component/build component/extraction good first issue kind/bug

Create a list of Lwt-related libraries, and link them from README ocsigen/lwt

An example of this is [lwt-parallel]( Also, many libraries have `_lwt` packages. Let's collect the most relevant ones, and link to them from the README, so users ca...

Created - 5 comments - docs easy

[easy] Document that Lwt_io.printf is more like sprintf than printf ocsigen/lwt

From `Lwt_io.printf` calls `ksprintf` internally. This has some surprising consequences: - `%!` doesn't really flush any...

Created - 5 comments - bug docs easy good first issue

Transpilation fastpack/fastpack

As of now, FastpackTranspiler supports a few, mostly non-standard syntax features (JSX, decorators) and some stage 3 features (spread). What is the goal of this project in terms of transpilation...

Created - 6 comments - good first task help wanted

`make install` installs coqide manpage with `-coqide no` coq/coq

<!-- Thank you for your contribution. Please complete the following information when reporting a bug. --> #### Version #### Operating system Linux #### Description of t...

Created - 6 comments - good first issue help wanted part: IDE part: installation

Add a .desktop file bcpierce00/unison

It would be great to add a .desktop file by default when installing the GUI version. Look [here]( for an example...

Created - 6 comments - easy help wanted minor

Accurate messages in exceptions raised by Lwt ocsigen/lwt

For example, trying this in the REPL ``` let _, r = Lwt.wait ();; Lwt.wakeup r ();; Lwt.wakeup r ();; ``` i.e. calling `Lwt.wakeup r ()` when `r` is already resolved, raises `Invalid_ar...

Created - 7 comments - bug easy

OSX GUI doesn't compile on 10.13 bcpierce00/unison

I'm experimenting with Unison on an OSX 10.13 machine. The text interface works fine, but compiling the GUI generates a bunch of warnings and then fails like this: 2017-11-24 12:19:06.176 ibtoo...

Created - 8 comments - good first issue help wanted important

[easy] Clarify Lwt.finalize documentation ocsigen/lwt

From > The documentation for Lwt.finalize states: > > > `finalize f g` returns the same result as `f ()` whether i...

Created - 8 comments - docs easy

Command to list available modules in an Esy environment esy/esy

We've added `esy ls-libs` command recently which allows to see what ocamlfind libraries are avaliable in the environment. That helps configuring build systems a lot (filling jbuilder's `(libraries ...

Created - 8 comments - good first issue

Displaying issues 1 - 30 of 37 in total