ssreflect - Re: [ssreflect] Docker images of coq-mathcomp-character

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] Docker images of coq-mathcomp-character

From: Emilio Jesús Gallego Arias <>
To: Erik Martin-Dorel <>
Cc: , , Cyril Cohen <>
Subject: Re: [ssreflect] Docker images of coq-mathcomp-character
Date: Fri, 08 Feb 2019 10:52:19 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=Pass
Ironport-phdr: 9a23:M8DiwxYB5Ss6vbPawAfXHFz/LSx+4OfEezUN459isYplN5qZoMmzbnLW6fgltlLVR4KTs6sC17KG9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa+bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjm58axlVAHnhzsGNz4h8WHYlMpwjL5AoBm8oxBz2pPYbJ2JOPZ7eK7WYNEUSndbXstJVyJPHJ6yb4wBD+QPP+lWrIfyqFQSohalGQmgGPnixiNUinLs36A31fkqHwHc3AwnGtIDqHvarND0NKcWUOC1y7HHwzHdYPNNwy/985DHfBE7rvGIWbJ/b8XRyU43GA7ZlFWQqJbqPyiI3ekKrWeW9OVhWOGzh2I9rAFxuDevy94qh4LUhYwV0kjJ+Th6zYs2P9G0VlB3bN++HJdNtSyWKpF6Tt4sTm12oCo216MKtJ2hcCUOxpkr3R3SZvOdf4SW7R/vSuCcKipiin1/YrKwnROy/FCgyuLiUsm0105HryVGn9XQrHwN0AbT6sefRvt8+EeuxyqP2hjO5uxHIk04j7TXJ4Agz7Iqi5Yes1nPEjXrlEj4kqOabkAk9fKp6+TjbLXmvJicN4pshw7gKakvlc+yDfgiPggJRWib9vyw1Kf/8k3hXLVKkvo2n7HCsJDBP8QUuKC5AwtL3Yk/9xayFCym0dQdnXkfNl1JYhOHj47zO1HPOv/0F/m/g07/2Atskt3cP76pJ5zXMnnF1ZvmZ7t5oxpR0gswi9VW/Y5VDPQNJ+j+Xmfwrt3ESBEjZV+a2eHiXfh414cfXlWtD7QLK5T9uFuM6+0oFMCWZYYO8GLwA+h1v7jpl3BvygxVRrWgwZZCMCPwJf9hOUjMJCO02o5QQ1dPhRI3SanRsHPHVDdSY3ioWKdttCFrUMShF4iRH9nx0ozE5z+yG9htXk4DEkqFQCX4J93CXO0DOnrLf51R1wccXL3kcLcPkBGjsAirmao3dqzT4CJK7J8=
Organization: X80 Heavy Industries

Dear Erik,

congratulations on this amazing work!

Porting some travis scripts I was wondering about the naming scheme:

> * mathcomp/mathcomp:1.7.0-coq-8.9 (opam switches: 4.05.0, 4.07.0+flambda)

vs

> * mathcomp/mathcomp-dev:coq-8.6 (opam switch: 4.02.3)

so indeed wouldn't it be more convenient this to be named:

mathcomp/mathcomp:dev-coq-8.6 ?

The thing is that I'd like to have a matrix with

COQ_VERSION=xxx
MATHCOMP_VERSION=yyy

and use a substitution such as
"mathcomp/mathcomp:$MATHCOMP_VERSION-coq-$COQ_VERSION"

Best regards,
E.

[ssreflect] Docker images of coq-mathcomp-character, Erik Martin-Dorel, 02/07/2019
- Re: [ssreflect] Docker images of coq-mathcomp-character, Emilio Jesús Gallego Arias, 02/08/2019
  - Re: [ssreflect] [mathcomp-dev] Docker images of coq-mathcomp-character, Emilio Jesús Gallego Arias, 02/08/2019
  - Re: [ssreflect] Docker images of coq-mathcomp-character, Erik Martin-Dorel, 02/08/2019
    - Re: [ssreflect] Docker images of coq-mathcomp-character, Emilio Jesús Gallego Arias, 02/09/2019
      - Re: [ssreflect] Docker images of coq-mathcomp-character, Erik Martin-Dorel, 02/09/2019

List archive

Re: [ssreflect] Docker images of coq-mathcomp-character