10 files changed, 79 insertions, 13 deletions
diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml
index 4e8130a..a9ff81a 100644
--- a/.github/workflows/nix-action.yml
+++ b/.github/workflows/nix-action.yml
@@ -39,7 +39,7 @@ jobs:
         matrix=$(nix-shell --arg do-nothing true --run nixTasks)
         echo ::set-output name=matrix::{\"task\":$(echo $matrix)}\"
 
-  main:
+  mathcomp:
     runs-on: ubuntu-latest
     needs:
     - setup
@@ -67,11 +67,11 @@ jobs:
       with:
         fetch-depth: 0
     - name: Building/fetching dependencies
-      run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies
+      run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job "_deps"
     - name: Building/fetching current project
-      run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job main
+      run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job mathcomp
 
-  shell:
+  mathcomp-single:
     runs-on: ubuntu-latest
     needs:
     - setup
@@ -99,7 +99,7 @@ jobs:
       with:
         fetch-depth: 0
     - name: Building/fetching dependencies
-      run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies
+      run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job _deps
     - name: Building/fetching current project
-      run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job shell
+      run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job mathcomp-single
 
diff --git a/.gitpod.Dockerfile b/.gitpod.Dockerfile
new file mode 100644
index 0000000..c5b5cc1
--- /dev/null
+++ b/.gitpod.Dockerfile
@@ -0,0 +1,27 @@
+FROM gitpod/workspace-full
+
+USER root
+
+# Install Nix
+RUN addgroup --system nixbld \
+  && adduser gitpod nixbld \
+  && for i in $(seq 1 30); do useradd -ms /bin/bash nixbld$i &&  adduser nixbld$i nixbld; done \
+  && mkdir -m 0755 /nix && chown gitpod /nix \
+  && mkdir -p /etc/nix && echo 'sandbox = false' > /etc/nix/nix.conf
+
+# Install Nix
+CMD /bin/bash -l
+USER gitpod
+ENV USER gitpod
+WORKDIR /home/gitpod
+
+RUN touch .bash_profile \
+ && curl https://nixos.org/releases/nix/nix-2.3.10/install | sh
+
+RUN echo '. /home/gitpod/.nix-profile/etc/profile.d/nix.sh' >> /home/gitpod/.bashrc
+
+# Install coq & math-comp environement
+RUN . /home/gitpod/.nix-profile/etc/profile.d/nix.sh \
+  && nix-env -iA cachix -f https://cachix.org/api/v1/install \
+  && cachix use coq \
+  && cachix use math-comp
diff --git a/.gitpod.yml b/.gitpod.yml
new file mode 100644
index 0000000..725060a
--- /dev/null
+++ b/.gitpod.yml
@@ -0,0 +1,19 @@
+---
+# The Docker image to run your workspace in. Defaults to gitpod/workspace-full
+image:
+  file: .gitpod.Dockerfile
+
+# Command to start on workspace startup (optional)
+tasks:
+  - before: nix-shell
+
+ports:
+  - port: 8000
+    onOpen: open-preview
+
+vscode:
+  extensions:
+    - bbenoist.Nix@1.0.1:TbrU16w37jLfkqA6h20vuQ==
+    - gares.coq-elpi-lang@0.0.4:fd+apIChnUwoQhvWFW33KA==
+    - gares.elpi-lang@0.1.1:Hq2+Ku1u3oO5KPtLqtFsIA==
+    - maximedenes.vscoq@0.3.4:scKF++aWERyqPMiIz8l02w==
+\ No newline at end of file
diff --git a/.nix/config.nix b/.nix/config.nix
index 5656f01..2f20a52 100644
--- a/.nix/config.nix
+++ b/.nix/config.nix
@@ -6,11 +6,11 @@
 
   ## The attribute to build, either from nixpkgs
   ## of from the overlays located in `.nix/coq-overlays`
-  coq-attribute = "mathcomp";
+  attribute = "mathcomp";
 
   ## If you want to select a different attribute
   ## to serve as a basis for nix-shell edit this
-  shell-coq-attribute = "mathcomp-single";
+  shell-attribute = "mathcomp-single";
 
   ## Indicate the relative location of your _CoqProject
   ## If not specified, it defaults to "_CoqProject"
@@ -18,7 +18,7 @@
 
   ## select an entry to build in the following `tasks` set
   ## defaults to "default"
-  select = "coq-8.13";
+  default-task = "coq-8.13";
 
   ## write one `tasks.name` attribute set per
   ## alternative configuration, the can be used to
diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix
index 0795edb..8fb74c6 100644
--- a/.nix/coq-nix-toolbox.nix
+++ b/.nix/coq-nix-toolbox.nix
@@ -1 +1 @@
-"152a643557a3a6a009b626a5def62a3c60952a43"
+"8fd39e891d8d5a74321b156d68bc3c615560dade"
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 4ea1df2..8a7a0b4 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -25,6 +25,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - in `path.v`, new lemmas: `sorted_pairwise(_in)`, `path_pairwise(_in)`,
   `cycle_all2rel(_in)`, `pairwise_sort`, and `sort_pairwise_stable`.
 
+- in `tuple.v`, added Canonical tuple for sort.
+
 - in `interval.v`, new lemmas: `ge_pinfty`, `le_ninfty`, `gt_pinfty`, `lt_ninfty`.
 
 - in `order.v`
diff --git a/_CoqProject b/_CoqProject
new file mode 100644
index 0000000..5493330
--- /dev/null
+++ b/_CoqProject
@@ -0,0 +1,10 @@
+-I mathcomp
+-R mathcomp mathcomp
+
+-arg -w -arg -projection-no-head-constant
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -notation-overridden
+-arg -w -arg +duplicate-clear
+-arg -w -arg +non-primitive-record
+-arg -w -arg +undeclared-scope
+-arg -w -arg -deprecated-hint-without-locality
diff --git a/default.nix b/default.nix
index a588f43..dbc0c1b 100644
--- a/default.nix
+++ b/default.nix
@@ -1,7 +1,7 @@
 { config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false,
-  update-nixpkgs ? false, ci-matrix ? false, ci-job ? null,
+  update-nixpkgs ? false, ci-matrix ? false,
   override ? {}, ocaml-override ? {}, global-override ? {},
-  ci ? (!isNull ci-job), inNixShell ? null, src ? ./.,
+  task ? null, job ? null, inNixShell ? null, src ? ./.,
 }@args:
 let auto = fetchGit {
   url = "https://github.com/coq-community/coq-nix-toolbox.git";
diff --git a/etc/utils/setup_gitpod.sh b/etc/utils/setup_gitpod.sh
new file mode 100755
index 0000000..f7538c0
--- /dev/null
+++ b/etc/utils/setup_gitpod.sh
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+mkdir -p .theia
+echo "{ \"coqtop.binPath\": \"$COQBIN\" }" > .theia/settings.json
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index f32793f..50a4d1e 100644
--- a/mathcomp/ssreflect/tuple.v
+++ b/mathcomp/ssreflect/tuple.v
@@ -1,7 +1,7 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
-From mathcomp Require Import seq choice fintype.
+From mathcomp Require Import seq choice fintype path.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -208,6 +208,10 @@ Lemma allpairs_tupleP f t (u : m.-tuple U) : @size rT (allpairs f t u) == n * m.
 Proof. by rewrite size_allpairs !size_tuple. Qed.
 Canonical allpairs_tuple f t u := Tuple (allpairs_tupleP f t u).
 
+Lemma sort_tupleP r t : size (sort r t) == n.
+Proof. by rewrite size_sort size_tuple. Qed.
+Canonical sort_tuple r t := Tuple (sort_tupleP r t).
+
 Definition thead (u : n.+1.-tuple T) := tnth u ord0.
 
 Lemma tnth0 x t : tnth [tuple of x :: t] ord0 = x.