Coq kanalo por Guix

de Julien Lepiller — ĵaŭ 27 Junio 2019

Kio estas Coq?

Coq estas pruvada asistilo. Ĝi estas disvolva medio kun programlingvo tre proksima al OCaml. Ĝi permesas skribi kune programojn kaj matematikajn asertojn. Coq ankaŭ enhavas taktikan programlingvon kiu permesas skribi demonstrojn de tiuj asertoj. Miksitante tiuj programlingvon, oni povas esprimi tre kompleksajn proprecojn pri programoj kaj demonstri ilin.

Ĉi tiu blogero nek estas kurso pri coq, nek estas enkonduko. Sed mi uzas coq kaj mi ankaŭ uzas vim por programado, do mi bezonas etendaĵon por uzi la coq sistemon en mia plej ŝatata midio.

Por fari tion, estis la etendaĵo Coquille kiu funkciis nur kun maljunaj versioj de coq, sed la projekto ne plu estas tre aktiva. Mi decidis lastajare ke mi bezonis ĝin, do me kreis forkon de coquille. Mi tradukis ĝin por neovim, kiu estis la unuan vi-forkon kiu povis uzi multajn fadenojn.

Etendaĵo, testoj kaj kanalo

Por programi tiu etendaĵo, mi fine devis uzi testojn por certigi mi ne skribas erarojn. Kvankam ili estas tre malplenaj, mi sciis ke mi bezonu subteni multajn versiojn de coq. Por fari tion, mi volis uzi Guix por krei mediojn kun diversaj versioj de coq.

Sed Guix nur enhavas une versio de ĉiu aplikaĵo, kaj coq ne estas escepto. Mi devis trovi manieron por havi multajn versiojn, sed ekstere de Guix. Por tio, mi povas uzi kanalon: eblas etendi Guix sen ŝanĝi ĝin. Estas tre facila krei kanalojn, do nun estas farita en framagit deponejo.

Uzado

Por uzi tiuj versioj, vi devos postemeti la kanalon al via kanallisto. Se la dosiero ~/.config/guix/channels.scm ne ekzistas, kreu ĝin kaj skribu:

(cons* (channel
   (name 'coq)
   (url https://framagit.org/tyreunom/guix-coq-channel.git))
  %default-channels)

Nun, post guix pull vi povus instali kaj uzi coq en multaj versioj. Vi povus listigi versioj de coq ĉi-maniere:

$ guix package -A ^coq$

coq	8.7.2	out	coq/coq.scm:98:2
coq	8.10+beta1	out	coq/coq.scm:166:2
coq	8.6.1	out	coq/coq.scm:36:2
coq	8.8.2	out	coq/coq.scm:149:2
coq	8.9.1	out	gnu/packages/coq.scm:44:2